lean2/examples/ex2.lean
Leonardo de Moura 5d2027d889 Add parse_lambda and parse_pi
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-18 12:34:00 -07:00

6 lines
No EOL
175 B
Text

Check fun x : Bool, x
Show fun x y : Bool, x
Show fun (A : Type) (x y : A), x = y
Check fun (A : Type) (x y : A), x = y
Check Pi (A B : Type), Type
Show Pi (A B : Type), A = B