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

chore: synthetic := false by default at sorryAx

Browse source
This commit is contained in:
Leonardo de Moura 2022-05-31 18:08:10 -07:00
parent 2b2f315fb9
commit 2e6dae01f0
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Prelude.lean
View file

@ -175,7 +175,7 @@ structure Subtype {α : Sort u} (p : α → Prop) where
/- Auxiliary axiom used to implement `sorry`. -/
@[extern "lean_sorry", neverExtract]
axiom sorryAx (α : Sort u) (synthetic := true) : α
axiom sorryAx (α : Sort u) (synthetic := false) : α
theorem eq_false_of_ne_true : {b : Bool} → Not (Eq b true) → Eq b false
| true, h => False.elim (h rfl)