michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

test(tests/lean): new test full of holes

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-02 16:31:52 -08:00
parent 9620b00e24
commit 502d9f47ac
2 changed files with 16 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
tests/lean/bad10.lean Normal file
View file

@ -0,0 +1,8 @@
SetOption pp::implicit true.
SetOption pp::colors false.
Variable N : Type.
Definition T (a : N) (f : _ -> _) (H : f a == a) : f (f _) == f _ :=
SubstP (fun x : N, f (f a) == _) (Refl (f (f _))) H.
Show Environment 1.

8
tests/lean/bad10.lean.expected.out Normal file
View file

@ -0,0 +1,8 @@
Set: pp::colors
Set: pp::unicode
Set: lean::pp::implicit
Set: pp::colors
Assumed: N
Defined: T
Definition T (a : N) (f : N → N) (H : f a == a) : f (f a) == f (f a) :=
@SubstP N (f a) a (λ x : N, f (f a) == f (f a)) (@Refl N (f (f a))) H