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

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2020-12-16 10:53:27 -08:00
parent a4901f131b
commit 0334bcb1bf
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
stage0/src/Init/Classical.lean generated
View file

@ -68,7 +68,7 @@ noncomputable def inhabitedOfExists {α : Sort u} {p : α → Prop} (h : ∃ x,
inhabitedOfNonempty (Exists.elim h (fun w hw => ⟨w⟩))
/- all propositions are Decidable -/
noncomputable def propDecidable (a : Prop) : Decidable a :=
@[scoped instance low] noncomputable def propDecidable (a : Prop) : Decidable a :=
choice <| match em a with
| Or.inl h => ⟨isTrue h⟩
| Or.inr h => ⟨isFalse h⟩