lean2/tests/lean/run/e2.lean
Leonardo de Moura 3e7dfa6212 fix(frontends/lean): infer type of definitions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-25 08:39:14 -07:00

2 lines
48 B
Text

definition Bool [inline] := Type.{0}
check Bool