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

test(kernel/typechecker): type checker

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-11-16 15:01:39 -08:00
parent 516c5c8fea
commit 390f7eaec8
2 changed files with 14 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
tests/lean/ty2.lean Normal file
View file

@ -0,0 +1,6 @@
Definition B : Type := Bool
Definition T : Type 1 := Type
Variable N : T
Variable x : N
Variable a : B
Axiom H : a

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

@ -0,0 +1,8 @@
Set: pp::colors
Set: pp::unicode
Defined: B
Defined: T
Assumed: N
Assumed: x
Assumed: a
Assumed: H