leanprover / lean4

Lean 4 programming language and theorem prover
https://lean-lang.org
Apache License 2.0
3.82k stars 325 forks source link

fix: remove `Subtype.instInhabited` #4055

Closed kmill closed 1 week ago

kmill commented 2 weeks ago

It has had a long history going back 10 years, but its time has come to an end since this instance is never applicable.

leanprover-community-mathlib4-bot commented 2 weeks ago

Mathlib CI status (docs):

kmill commented 2 weeks ago

!bench

leanprover-bot commented 2 weeks ago

Here are the benchmark results for commit 24b472541c2fdb91fe573654b095aef50b46f6ed. There were no significant changes against commit b470eb522bfd68ca96938c23f6a1bce79da8a99f.