diff --git a/library/init/nat.lean b/library/init/nat.lean index 7580f00b76..6fa94f2558 100644 --- a/library/init/nat.lean +++ b/library/init/nat.lean @@ -14,7 +14,7 @@ namespace nat {C : ℕ → Type} (n : ℕ) (H₁ : C 0) (H₂ : Π (a : ℕ), C a → C (succ a)) : C n := nat.rec H₁ H₂ n - protected definition induction_on + protected theorem induction_on {C : ℕ → Prop} (n : ℕ) (H₁ : C 0) (H₂ : Π (a : ℕ), C a → C (succ a)) : C n := nat.rec H₁ H₂ n diff --git a/library/init/tactic.lean b/library/init/tactic.lean index 6fad9f50fd..9d54fc421d 100644 --- a/library/init/tactic.lean +++ b/library/init/tactic.lean @@ -154,8 +154,6 @@ definition repeat1 (t : tactic) : tactic := and_then t (repeat t) definition focus (t : tactic) : tactic := focus_at t 0 definition determ (t : tactic) : tactic := at_most t 1 -- definition trivial : tactic := or_else (or_else (apply eq.refl) (apply true.intro)) assumption -definition do (n : num) (t : tactic) : tactic := -nat.rec id (λn t', and_then t t') (nat.of_num n) end tactic -- tactic_infixl `;`:15 := tactic.and_then -- tactic_notation T1 `:`:15 T2 := tactic.focus (tactic.and_then T1 (tactic.all_goals T2)) diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index a09c5f99b7..729bbfbcb1 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -27,6 +27,7 @@ Author: Leonardo de Moura #include "library/definitional/equations.h" #include "library/compiler/inliner.h" #include "library/compiler/vm_compiler.h" +#include "library/vm/vm.h" #include "frontends/lean/parser.h" #include "frontends/lean/util.h" #include "frontends/lean/tokens.h" @@ -1170,7 +1171,7 @@ class definition_cmd_fn { } void compile_decl() { - if (m_is_noncomputable || m_is_inline || !is_definition()) + if (m_is_noncomputable || m_is_inline || !is_definition() || is_vm_builtin_function(m_real_name)) return; try { declaration d = m_env.get(m_real_name); diff --git a/src/library/constants.cpp b/src/library/constants.cpp index 6039c864c6..dbeae0c62c 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -116,7 +116,9 @@ name const * g_nat_has_decidable_eq = nullptr; name const * g_nat_decidable_le = nullptr; name const * g_nat_decidable_lt = nullptr; name const * g_nat_cases_on = nullptr; +name const * g_nat_rec_on = nullptr; name const * g_nat_no_confusion = nullptr; +name const * g_nat_no_confusion_type = nullptr; name const * g_ne = nullptr; name const * g_neg = nullptr; name const * g_norm_num_add1 = nullptr; @@ -403,7 +405,9 @@ void initialize_constants() { g_nat_decidable_le = new name{"nat", "decidable_le"}; g_nat_decidable_lt = new name{"nat", "decidable_lt"}; g_nat_cases_on = new name{"nat", "cases_on"}; + g_nat_rec_on = new name{"nat", "rec_on"}; g_nat_no_confusion = new name{"nat", "no_confusion"}; + g_nat_no_confusion_type = new name{"nat", "no_confusion_type"}; g_ne = new name{"ne"}; g_neg = new name{"neg"}; g_norm_num_add1 = new name{"norm_num", "add1"}; @@ -691,7 +695,9 @@ void finalize_constants() { delete g_nat_decidable_le; delete g_nat_decidable_lt; delete g_nat_cases_on; + delete g_nat_rec_on; delete g_nat_no_confusion; + delete g_nat_no_confusion_type; delete g_ne; delete g_neg; delete g_norm_num_add1; @@ -978,7 +984,9 @@ name const & get_nat_has_decidable_eq_name() { return *g_nat_has_decidable_eq; } name const & get_nat_decidable_le_name() { return *g_nat_decidable_le; } name const & get_nat_decidable_lt_name() { return *g_nat_decidable_lt; } name const & get_nat_cases_on_name() { return *g_nat_cases_on; } +name const & get_nat_rec_on_name() { return *g_nat_rec_on; } name const & get_nat_no_confusion_name() { return *g_nat_no_confusion; } +name const & get_nat_no_confusion_type_name() { return *g_nat_no_confusion_type; } name const & get_ne_name() { return *g_ne; } name const & get_neg_name() { return *g_neg; } name const & get_norm_num_add1_name() { return *g_norm_num_add1; } diff --git a/src/library/constants.h b/src/library/constants.h index 4e5c20ced8..1e07466d39 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -118,7 +118,9 @@ name const & get_nat_has_decidable_eq_name(); name const & get_nat_decidable_le_name(); name const & get_nat_decidable_lt_name(); name const & get_nat_cases_on_name(); +name const & get_nat_rec_on_name(); name const & get_nat_no_confusion_name(); +name const & get_nat_no_confusion_type_name(); name const & get_ne_name(); name const & get_neg_name(); name const & get_norm_num_add1_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index 74f658405c..ba79bc84ae 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -111,7 +111,9 @@ nat.has_decidable_eq nat.decidable_le nat.decidable_lt nat.cases_on +nat.rec_on nat.no_confusion +nat.no_confusion_type ne neg norm_num.add1 diff --git a/src/library/vm/vm_nat.cpp b/src/library/vm/vm_nat.cpp index ff92463952..a3c6f28c72 100644 --- a/src/library/vm/vm_nat.cpp +++ b/src/library/vm/vm_nat.cpp @@ -178,6 +178,16 @@ static void nat_decidable_lt(vm_state & s) { } } +static void nat_rec(vm_state &) { + /* recursors are implemented by the compiler */ + lean_unreachable(); +} + +static void nat_no_confusion(vm_state &) { + /* no_confusion is implemented by the compiler */ + lean_unreachable(); +} + void initialize_vm_nat() { declare_vm_builtin(get_nat_succ_name(), 1, nat_succ); declare_vm_builtin(get_nat_add_name(), 2, nat_add); @@ -189,6 +199,10 @@ void initialize_vm_nat() { declare_vm_builtin(get_nat_has_decidable_eq_name(), 2, nat_has_decidable_eq); declare_vm_builtin(get_nat_decidable_le_name(), 2, nat_decidable_le); declare_vm_builtin(get_nat_decidable_lt_name(), 2, nat_decidable_lt); + declare_vm_builtin(get_nat_cases_on_name(), 4, nat_rec); + declare_vm_builtin(get_nat_rec_on_name(), 4, nat_rec); + declare_vm_builtin(get_nat_no_confusion_name(), 5, nat_no_confusion); + declare_vm_builtin(get_nat_no_confusion_type_name(), 3, nat_no_confusion); } void finalize_vm_nat() {