From d444b5ef490771ffdbfdfc563ab74115b23238c3 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 15 Jan 2019 17:42:09 +0100 Subject: [PATCH] chore(library/init/core): move `sorry_ax` up (temporarily) to get error recovery sooner --- library/init/core.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/library/init/core.lean b/library/init/core.lean index d1f672c11f..3baa39d6a9 100644 --- a/library/init/core.lean +++ b/library/init/core.lean @@ -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) : α