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

refactor(library/logic/core/cast): cleanup

Browse source
This commit is contained in:
Leonardo de Moura 2014-09-09 19:11:03 -07:00
parent 570879b55f
commit b4d765ff2e
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
library/logic/core/cast.lean
View file

@ -12,14 +12,14 @@ definition cast {A B : Type} (H : A = B) (a : A) : B :=
eq.rec a H
theorem cast_refl {A : Type} (a : A) : cast (eq.refl A) a = a :=
eq.refl (cast (eq.refl A) a)
rfl
theorem cast_proof_irrel {A B : Type} (H1 H2 : A = B) (a : A) : cast H1 a = cast H2 a :=
eq.refl (cast H1 a)
rfl
theorem cast_eq {A : Type} (H : A = A) (a : A) : cast H a = a :=
calc cast H a = cast (eq.refl A) a : cast_proof_irrel H (eq.refl A) a
... = a : cast_refl a
calc cast H a = cast (eq.refl A) a : rfl
... = a : rfl
definition heq {A B : Type} (a : A) (b : B) :=
∃H, cast H a = b