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

fix(library/logic/heq): heq.to_eq must be transparent because it is needed in the 'inversion' tactic used by definitional package

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-28 23:49:17 -08:00
parent cab99e2e22
commit d7042c4618
2 changed files with 6 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/data/vector.lean
View file

@ -188,7 +188,7 @@ namespace vector
vector.induction_on v
rfl
(λ h n t ih, calc
last (concat (h :: t) a) = last (concat t a) : last_cons
last (concat (h :: t) a) = last (concat t a) : rfl
... = a : ih)
end vector

12
library/logic/heq.lean
View file

@ -19,18 +19,16 @@ namespace heq
theorem symm (H : a == b) : b == a :=
subst H (refl a)
theorem type_eq (H : a == b) : A = B :=
subst H (eq.refl A)
definition type_eq (H : a == b) : A = B :=
heq.rec_on H (eq.refl A)
theorem from_eq (H : a = a') : a == a' :=
eq.subst H (refl a)
theorem to_eq (H : a == a') : a = a' :=
definition to_eq (H : a == a') : a = a' :=
have H₁ : ∀ (Ht : A = A), eq.rec_on Ht a = a, from
take Ht, eq.refl (eq.rec_on Ht a),
have H₂ : ∀ (Ht : A = A), eq.rec_on Ht a = a', from
heq.rec_on H H₁,
H₂ (type_eq H)
λ Ht, eq.refl (eq.rec_on Ht a),
heq.rec_on H H₁ (eq.refl A)
theorem trans (H₁ : a == b) (H₂ : b == c) : a == c :=
subst H₂ H₁