fix(tests/lean): add parenthesis
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
f0e149d77b
commit
c1c1af4b98
4 changed files with 11 additions and 11 deletions
|
@ -11,9 +11,9 @@ p f : Bool
|
|||
g a : Bool
|
||||
Defined: c2
|
||||
Assumed: b
|
||||
c2::explicit : Π (T : Type), Type 3 → T → Type 3
|
||||
c2::explicit : Π (T : Type), (Type 3) → T → (Type 3)
|
||||
Assumed: g2
|
||||
g2 : (c2 Type 2 b) → Bool
|
||||
g2 : (c2 (Type 2) b) → Bool
|
||||
Assumed: a2
|
||||
g2 a2 : Bool
|
||||
λ x : c2 Type 1 b, g2 x : (c2 Type 1 b) → Bool
|
||||
λ x : c2 (Type 1) b, g2 x : (c2 (Type 1) b) → Bool
|
||||
|
|
|
@ -3,7 +3,7 @@
|
|||
Assumed: x
|
||||
x : Type U+3 ⊔ M+2 ⊔ 3
|
||||
Assumed: f
|
||||
f : Type U+10 → Type
|
||||
f : (Type U+10) → Type
|
||||
f x : Type
|
||||
Type 4 : Type 5
|
||||
x : Type U+3 ⊔ M+2 ⊔ 3
|
||||
|
@ -14,9 +14,9 @@ Type U ⊔ M : Type U+1 ⊔ M+1
|
|||
Type U ⊔ M ⊔ 3 : Type U+1 ⊔ M+1 ⊔ 4
|
||||
Type U+1 ⊔ M ⊔ 3
|
||||
Type U+1 ⊔ M ⊔ 3 : Type U+2 ⊔ M+1 ⊔ 4
|
||||
Type U → Type 5
|
||||
Type U → Type 5 : Type U+1 ⊔ 6
|
||||
Type M ⊔ 3 → Type U+5 : Type M+1 ⊔ 4 ⊔ U+6
|
||||
Type M ⊔ 3 → Type U → Type 5
|
||||
Type M ⊔ 3 → Type U → Type 5 : Type M+1 ⊔ 6 ⊔ U+1
|
||||
(Type U) → (Type 5)
|
||||
(Type U) → (Type 5) : Type U+1 ⊔ 6
|
||||
(Type M ⊔ 3) → (Type U+5) : Type M+1 ⊔ 4 ⊔ U+6
|
||||
(Type M ⊔ 3) → (Type U) → (Type 5)
|
||||
(Type M ⊔ 3) → (Type U) → (Type 5) : Type M+1 ⊔ 6 ⊔ U+1
|
||||
Type U
|
||||
|
|
|
@ -11,7 +11,7 @@ f::explicit ((N → N) → N → N) (λ x : N → N, x) (λ y : N → N, y)
|
|||
EqNice::explicit N n1 n2
|
||||
f::explicit N n1 n2 : N
|
||||
Congr::explicit :
|
||||
Π (A : Type U) (B : A → Type U) (f g : Π x : A, B x) (a b : A), (f = g) → (a = b) → ((f a) = (g b))
|
||||
Π (A : Type U) (B : A → (Type U)) (f g : Π x : A, B x) (a b : A), (f = g) → (a = b) → ((f a) = (g b))
|
||||
f::explicit N n1 n2
|
||||
Assumed: a
|
||||
Assumed: b
|
||||
|
|
|
@ -7,5 +7,5 @@ a ≃ b
|
|||
a ≃ b : Bool
|
||||
Set: lean::pp::implicit
|
||||
heq::explicit N a b
|
||||
heq::explicit Type 2 Type 1 Type 1
|
||||
heq::explicit (Type 2) (Type 1) (Type 1)
|
||||
heq::explicit Bool ⊤ ⊥
|
||||
|
|
Loading…
Reference in a new issue