max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: remove done

Browse source
This commit is contained in:
Leonardo de Moura 2021-05-15 18:57:27 -07:00
parent c7096f54a2
commit 4dabfef0e3
1 changed files with 0 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Init/Core.lean
View file

@ -272,7 +272,6 @@ theorem heqOfEqRecEq {α β : Sort u} {a : α} {b : β} (h₁ : α = β) (h₂ :
subst h₁
apply heqOfEq
exact h₂
done
theorem castHEq {α β : Sort u} : (h : α = β) → (a : α) → cast h a ≅ a
| rfl, a => HEq.refl a