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

fix: prove decidable_of_decidable_of_eq without cast

Browse source
This commit is contained in:
Mario Carneiro 2022-08-28 10:22:51 -04:00 • committed by Leonardo de Moura
parent d4c7d0f266
commit f93914e613
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/Core.lean
View file

@ -431,8 +431,8 @@ variable {p q : Prop}
else
isFalse fun hq => absurd (Iff.mpr h hq) hp
@[inline] def decidable_of_decidable_of_eq [hp : Decidable p] (h : p = q) : Decidable q :=
h ▸ hp
@[inline] def decidable_of_decidable_of_eq [Decidable p] (h : p = q) : Decidable q :=
decidable_of_decidable_of_iff (p := p) (h ▸ Iff.rfl)
end
@[macroInline] instance {p q} [Decidable p] [Decidable q] : Decidable (p → q) :=