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

fix(tests/lean): adjust expected results, the new result is also acceptable

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-10-24 17:54:09 -07:00
parent e3efe39eeb
commit e55fb4f165
2 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
tests/lean/elab4.lean.expected.out
View file

@ -12,7 +12,7 @@ Definition D::explicit (A A' : Type) (B : A → Type) (B' : A' → Type) (H : (
A' :=
D H
Variable R {A A' : Type} {B : A → Type} {B' : A' → Type} (H : (Π x : A, B x) = (Π x : A', B' x)) (a : A) :
(B a) = (B' (C::explicit A A' (D::explicit A A' B B' H) a))
(B a) = (B' (C::explicit A A' (D::explicit A A' (λ x : A, B x) (λ x : A', B' x) H) a))
Definition R::explicit (A A' : Type)
(B : A → Type)
(B' : A' → Type)
@ -20,4 +20,4 @@ Definition R::explicit (A A' : Type)
(a : A) : (B a) = (B' (C (D H) a)) :=
R H a
Theorem R2 (A1 A2 B1 B2 : Type) (H : A1 → B1 = A2 → B2) (a : A1) : B1 = B2 :=
R::explicit A1 A2 (λ a : A1, B1) (λ _ : A2, B2) H a
R::explicit A1 A2 (λ x : A1, B1) (λ x : A2, B2) H a

4
tests/lean/elab5.lean.expected.out
View file

@ -12,7 +12,7 @@ Definition D::explicit (A A' : Type) (B : A → Type) (B' : A' → Type) (H : (
A' :=
D H
Variable R {A A' : Type} {B : A → Type} {B' : A' → Type} (H : (Π x : A, B x) = (Π x : A', B' x)) (a : A) :
(B a) = (B' (C::explicit A A' (D::explicit A A' B B' H) a))
(B a) = (B' (C::explicit A A' (D::explicit A A' (λ x : A, B x) (λ x : A', B' x) H) a))
Definition R::explicit (A A' : Type)
(B : A → Type)
(B' : A' → Type)
@ -20,4 +20,4 @@ Definition R::explicit (A A' : Type)
(a : A) : (B a) = (B' (C (D H) a)) :=
R H a
Theorem R2 (A1 A2 B1 B2 : Type) (H : A1 → B1 = A2 → B2) (a : A1) : B1 = B2 :=
R::explicit A1 A2 (λ _ : A1, B1) (λ _ : A2, B2) H a
R::explicit A1 A2 (λ x : A1, B1) (λ x : A2, B2) H a