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

fix: invalid proof

Browse source
This commit is contained in:
Leonardo de Moura 2022-02-25 07:17:31 -08:00
parent db38bc4043
commit c9471ea029
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Init/Prelude.lean
View file

@ -204,7 +204,8 @@ class inductive Nonempty (α : Sort u) : Prop where
axiom Classical.choice {α : Sort u} : Nonempty α → α
protected def Nonempty.elim {α : Sort u} {p : Prop} (h₁ : Nonempty α) (h₂ : α → p) : p :=
h₂ h₁.1
match h₁ with
| intro a => h₂ a
instance {α : Sort u} [Inhabited α] : Nonempty α :=
⟨default⟩