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

chore(library/init/core): move sorry_ax up (temporarily) to get error recovery sooner

Browse source
This commit is contained in:
Sebastian Ullrich 2019-01-15 17:42:09 +01:00
parent cead81fcea
commit d444b5ef49
1 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
library/init/core.lean
View file

@ -317,6 +317,11 @@ inductive nat
| zero : nat
| succ (n : nat) : nat
/- Auxiliary axiom used to implement `sorry`.
TODO: add this theorem on-demand. That is,
we should only add it if after the first error. -/
constant sorry_ax (α : Sort u) (synthetic := tt) : α
/- Declare builtin and reserved notation -/
class has_zero (α : Type u) := (zero : α)
@ -2169,8 +2174,3 @@ theorem by_contradiction {p : Prop} (h : ¬p → false) : p :=
decidable.by_contradiction h
end classical
/- Auxiliary axiom used to implement `sorry`.
TODO: add this theorem on-demand. That is,
we should only add it if after the first error. -/
constant sorry_ax (α : Sort u) (synthetic := tt) : α