test(conversion): add more conversion tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
0783805671
commit
29ad71f9fc
2 changed files with 41 additions and 0 deletions
22
tests/lean/conv.lean
Normal file
22
tests/lean/conv.lean
Normal file
|
@ -0,0 +1,22 @@
|
|||
|
||||
|
||||
|
||||
Definition id (A : Type) : Type U := A.
|
||||
Variable p : (Int -> Int) -> Bool.
|
||||
Check fun (x : id Int), x.
|
||||
Variable f : (id Int) -> (id Int).
|
||||
Check p f.
|
||||
|
||||
Definition c (A : Type 3) : Type 3 := Type 1.
|
||||
Variable g : (c (Type 2)) -> Bool.
|
||||
Variable a : (c (Type 1)).
|
||||
Check g a.
|
||||
|
||||
Definition c2 {T : Type} (A : Type 3) (a : T) : Type 3 := Type 1
|
||||
Variable b : Int
|
||||
Check c2::explicit
|
||||
Variable g2 : (c2 (Type 2) b) -> Bool
|
||||
Check g2
|
||||
Variable a2 : (c2 (Type 1) b).
|
||||
Check g2 a2
|
||||
Check fun x : (c2 (Type 1) b), g2 x
|
19
tests/lean/conv.lean.expected.out
Normal file
19
tests/lean/conv.lean.expected.out
Normal file
|
@ -0,0 +1,19 @@
|
|||
Set: pp::colors
|
||||
Set: pp::unicode
|
||||
Defined: id
|
||||
Assumed: p
|
||||
λ x : id ℤ, x : (id ℤ) → (id ℤ)
|
||||
Assumed: f
|
||||
p f : Bool
|
||||
Defined: c
|
||||
Assumed: g
|
||||
Assumed: a
|
||||
g a : Bool
|
||||
Defined: c2
|
||||
Assumed: b
|
||||
c2::explicit : Π (T : Type), Type 3 → T → Type 3
|
||||
Assumed: g2
|
||||
g2 : (c2 Type 2 b) → Bool
|
||||
Assumed: a2
|
||||
g2 a2 : Bool
|
||||
λ x : c2 Type 1 b, g2 x : (c2 Type 1 b) → Bool
|
Loading…
Reference in a new issue