fix(tests/lean): adjust tests output to reflect recent changes in the pretty printer

This commit is contained in:
Leonardo de Moura 2015-05-08 11:11:00 -07:00
parent 3aac370629
commit 746e6dc0ff
3 changed files with 8 additions and 8 deletions

View file

@ -11,5 +11,5 @@ P : f a⁻¹ * f a = 1
583.lean:27:8: error: failed to add declaration 'group_hom.hom_map_inv' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (A : Type) (B : Type) (s1 : …) (s2 : …) (f : …) (Hom : …) (a : A),
have P [visible] : …, from …,
assert P : …, from …,
?M_1

View file

@ -1,7 +1,7 @@
have e1 [visible] : a = b, from H1,
assert e1 : a = b, from H1,
have e2 : a = c, from e1 ⬝ H2,
have e3 : c = a, from e2 ⁻¹,
have e4 [visible] : b = a, from e1 ⁻¹,
have e3 : c = a, from e2⁻¹,
assert e4 : b = a, from e1⁻¹,
have e5 : b = c, from e4 ⬝ e2,
have e6 : a = a, from H1 ⬝ H2 ⬝ H2 ⁻¹ ⬝ H1 ⁻¹ ⬝ H1 ⬝ H2 ⬝ H2 ⁻¹ ⬝ H1 ⁻¹,
e3 ⬝ e2 :

View file

@ -1,8 +1,8 @@
show a = c, from H1 ⬝ H2 : a = c
------------
have e1 [visible] : a = b, from H1,
assert e1 : a = b, from H1,
have e2 : a = c, from e1 ⬝ H2,
have e3 : c = a, from e2 ⁻¹,
have e4 [visible] : b = a, from e1 ⁻¹,
show b = c, from e1 ⁻¹ ⬝ e2 :
have e3 : c = a, from e2⁻¹,
assert e4 : b = a, from e1⁻¹,
show b = c, from e1⁻¹ ⬝ e2 :
b = c