Skip to content

Commit

Permalink
fix: remove Subtype.instInhabited
Browse files Browse the repository at this point in the history
It has a long history going back [10 years](leanprover-community/lean@3afad10#diff-4e22e2bb74f004d2ff7cdabcb5c01429abbc906e20befe2517679e257b4387e4R41), this instance cannot fire with the current system.
  • Loading branch information
kmill committed May 2, 2024
1 parent d3e0049 commit f44f3e4
Showing 1 changed file with 0 additions and 3 deletions.
3 changes: 0 additions & 3 deletions src/Init/Core.lean
Original file line number Diff line number Diff line change
Expand Up @@ -1114,9 +1114,6 @@ theorem eta (a : {x // p x}) (h : p (val a)) : mk (val a) h = a := by
cases a
exact rfl

instance {α : Type u} {p : α → Prop} {a : α} (h : p a) : Inhabited {x // p x} where
default := ⟨a, h⟩

instance {α : Type u} {p : α → Prop} [DecidableEq α] : DecidableEq {x : α // p x} :=
fun ⟨a, h₁⟩ ⟨b, h₂⟩ =>
if h : a = b then isTrue (by subst h; exact rfl)
Expand Down

0 comments on commit f44f3e4

Please sign in to comment.