test(frontends/lean): add 'l = nil' test

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-10-29 16:30:03 -07:00
parent 4dd6cead83
commit e3228b1f5c
2 changed files with 16 additions and 0 deletions

7
tests/lean/eq2.lean Normal file
View file

@ -0,0 +1,7 @@
Variable List : Type -> Type
Variable nil {A : Type} : List A
Variable cons {A : Type} (head : A) (tail : List A) : List A
Variable l : List Int.
Check l = nil.
Set pp::implicit true
Check l = nil.

View file

@ -0,0 +1,9 @@
Set: pp::colors
Set: pp::unicode
Assumed: List
Assumed: nil
Assumed: cons
Assumed: l
l = nil : Bool
Set: lean::pp::implicit
eq::explicit (List ) l (nil::explicit ) : Bool