From 1e1161138894d1440cd5abbda3b6d722956c765a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 12 Apr 2018 13:29:06 -0700 Subject: [PATCH] chore(library): cleanup constants.txt --- library/init/meta/comp_value_tactics.lean | 8 +- script/gen_constants_cpp.py | 2 +- src/library/comp_val.cpp | 106 ----- src/library/comp_val.h | 13 - src/library/constants.cpp | 456 ---------------------- src/library/constants.h | 114 ------ src/library/constants.txt | 114 ------ src/library/vm/vm.cpp | 7 - src/library/vm/vm.h | 2 - src/library/vm/vm_expr.cpp | 5 - src/library/vm/vm_io.cpp | 5 +- tests/lean/run/check_constants.lean | 248 ++++++++++++ 12 files changed, 251 insertions(+), 829 deletions(-) create mode 100644 tests/lean/run/check_constants.lean diff --git a/library/init/meta/comp_value_tactics.lean b/library/init/meta/comp_value_tactics.lean index af3617cfb1..64da65f88e 100644 --- a/library/init/meta/comp_value_tactics.lean +++ b/library/init/meta/comp_value_tactics.lean @@ -12,7 +12,6 @@ meta constant mk_nat_val_le_proof : expr → expr → option expr meta constant mk_fin_val_ne_proof : expr → expr → option expr meta constant mk_char_val_ne_proof : expr → expr → option expr meta constant mk_string_val_ne_proof : expr → expr → option expr -meta constant mk_int_val_ne_proof : expr → expr → option expr namespace tactic open expr @@ -51,11 +50,6 @@ do t ← target >>= instantiate_mvars, pr ← mk_string_val_ne_proof a b, exact pr) <|> - (do is_def_eq type (const `int []), - (a, b) ← is_ne t, - pr ← mk_int_val_ne_proof a b, - exact pr) - <|> (do type ← whnf type, guard (is_napp_of type `fin 1), (a, b) ← is_ne t, @@ -68,7 +62,7 @@ end tactic namespace tactic namespace interactive -/-- Close goals of the form `n ≠ m` when `n` and `m` have type `nat`, `char`, `string`, `int` or `fin sz`, +/-- Close goals of the form `n ≠ m` when `n` and `m` have type `nat`, `char`, `string`, or `fin sz`, and they are literals. It also closes goals of the form `n < m`, `n > m`, `n ≤ m` and `n ≥ m` for `nat`. If the foal is of the form `n = m`, then it tries to close it using reflexivity. -/ meta def comp_val := tactic.comp_val diff --git a/script/gen_constants_cpp.py b/script/gen_constants_cpp.py index 1245dc03a1..a2330b4a23 100755 --- a/script/gen_constants_cpp.py +++ b/script/gen_constants_cpp.py @@ -88,7 +88,7 @@ def main(argv=None): f.write('}\n') with open(tst_file, 'w') as f: f.write('-- DO NOT EDIT, automatically generated file, generator scripts/gen_constants_cpp.py\n') - f.write("import smt system.io\n") + f.write("import system.io\n") f.write("open tactic\n"); f.write("meta def script_check_id (n : name) : tactic unit :=\n"); f.write("do env ← get_env, (env^.get n >> return ()) <|> (guard $ env^.is_namespace n) <|> (attribute.get_instances n >> return ()) <|> fail (\"identifier '\" ++ to_string n ++ \"' is not a constant, namespace nor attribute\")\n"); diff --git a/src/library/comp_val.cpp b/src/library/comp_val.cpp index 765441bcae..b74cc426f3 100644 --- a/src/library/comp_val.cpp +++ b/src/library/comp_val.cpp @@ -207,116 +207,10 @@ optional mk_string_val_ne_proof(expr a, expr b) { return none_expr(); } -optional mk_int_val_nonneg_proof(expr const & a) { - if (auto a1 = is_bit0(a)) { - if (auto pr = mk_int_val_nonneg_proof(*a1)) - return some_expr(mk_app(mk_constant(get_int_bit0_nonneg_name()), *a1, *pr)); - } else if (auto a1 = is_bit1(a)) { - if (auto pr = mk_int_val_nonneg_proof(*a1)) - return some_expr(mk_app(mk_constant(get_int_bit1_nonneg_name()), *a1, *pr)); - } else if (is_one(a)) { - return some_expr(mk_constant(get_int_one_nonneg_name())); - } else if (is_zero(a)) { - return some_expr(mk_constant(get_int_zero_nonneg_name())); - } - return none_expr(); -} - -optional mk_int_val_pos_proof(expr const & a) { - if (auto a1 = is_bit0(a)) { - if (auto pr = mk_int_val_pos_proof(*a1)) - return some_expr(mk_app(mk_constant(get_int_bit0_pos_name()), *a1, *pr)); - } else if (auto a1 = is_bit1(a)) { - if (auto pr = mk_int_val_nonneg_proof(*a1)) - return some_expr(mk_app(mk_constant(get_int_bit1_pos_name()), *a1, *pr)); - } else if (is_one(a)) { - return some_expr(mk_constant(get_int_one_pos_name())); - } - return none_expr(); -} - -/* Given a nonnegative int numeral a, return a pair (n, H) - where n is a nat numeral, and (H : nat_abs a = n) */ -optional mk_nat_abs_eq(expr const & a) { - if (is_zero(a)) { - return optional(mk_pair(mk_nat_zero(), mk_constant(get_int_nat_abs_zero_name()))); - } else if (is_one(a)) { - return optional(mk_pair(mk_nat_one(), mk_constant(get_int_nat_abs_one_name()))); - } else if (auto a1 = is_bit0(a)) { - if (auto p = mk_nat_abs_eq(*a1)) - return optional(mk_pair(mk_nat_bit0(p->first), - mk_app(mk_constant(get_int_nat_abs_bit0_step_name()), *a1, p->first, p->second))); - } else if (auto a1 = is_bit1(a)) { - if (auto p = mk_nat_abs_eq(*a1)) { - expr new_n = mk_nat_bit1(p->first); - expr Hnonneg = *mk_int_val_nonneg_proof(*a1); - expr new_H = mk_app(mk_constant(get_int_nat_abs_bit1_nonneg_step_name()), *a1, p->first, Hnonneg, p->second); - return optional(mk_pair(new_n, new_H)); - } - } - return optional(); -} - -/* Given nonneg int numerals a and b, create a proof for a != b IF they are not equal. */ -optional mk_int_nonneg_val_ne_proof(expr const & a, expr const & b) { - auto p1 = mk_nat_abs_eq(a); - if (!p1) return none_expr(); - auto p2 = mk_nat_abs_eq(b); - if (!p2) return none_expr(); - auto Ha_nonneg = mk_int_val_nonneg_proof(a); - if (!Ha_nonneg) return none_expr(); - auto Hb_nonneg = mk_int_val_nonneg_proof(b); - if (!Hb_nonneg) return none_expr(); - auto H_nat_ne = mk_nat_val_ne_proof(p1->first, p2->first); - if (!H_nat_ne) return none_expr(); - expr H = mk_app({mk_constant(get_int_ne_of_nat_ne_nonneg_case_name()), a, b, p1->first, p2->first, - *Ha_nonneg, *Hb_nonneg, p1->second, p2->second, *H_nat_ne}); - return some_expr(H); -} - -optional mk_int_val_ne_proof(expr const & a, expr const & b) { - if (auto a1 = is_neg(a)) { - if (auto b1 = is_neg(b)) { - auto H = mk_int_nonneg_val_ne_proof(*a1, *b1); - if (!H) return none_expr(); - return some_expr(mk_app(mk_constant(get_int_ne_neg_of_ne_name()), *a1, *b1, *H)); - } else { - if (is_zero(b)) { - auto H = mk_int_nonneg_val_ne_proof(*a1, b); - if (!H) return none_expr(); - return some_expr(mk_app(mk_constant(get_int_neg_ne_zero_of_ne_name()), *a1, *H)); - } else { - auto Ha1_nonneg = mk_int_val_pos_proof(*a1); - if (!Ha1_nonneg) return none_expr(); - auto Hb_nonneg = mk_int_val_pos_proof(b); - if (!Hb_nonneg) return none_expr(); - return some_expr(mk_app(mk_constant(get_int_neg_ne_of_pos_name()), *a1, b, *Ha1_nonneg, *Hb_nonneg)); - } - } - } else { - if (auto b1 = is_neg(b)) { - if (is_zero(a)) { - auto H = mk_int_nonneg_val_ne_proof(a, *b1); - if (!H) return none_expr(); - return some_expr(mk_app(mk_constant(get_int_zero_ne_neg_of_ne_name()), *b1, *H)); - } else { - auto Ha_nonneg = mk_int_val_pos_proof(a); - if (!Ha_nonneg) return none_expr(); - auto Hb1_nonneg = mk_int_val_pos_proof(*b1); - return some_expr(mk_app(mk_constant(get_int_ne_neg_of_pos_name()), a, *b1, *Ha_nonneg, *Hb1_nonneg)); - } - } else { - return mk_int_nonneg_val_ne_proof(a, b); - } - } -} - optional mk_val_ne_proof(type_context_old & ctx, expr const & a, expr const & b) { expr type = ctx.infer(a); if (ctx.is_def_eq(type, mk_nat_type())) return mk_nat_val_ne_proof(a, b); - if (ctx.is_def_eq(type, mk_int_type())) - return mk_int_val_ne_proof(a, b); if (ctx.is_def_eq(type, mk_constant(get_char_name()))) return mk_char_val_ne_proof(a, b); if (ctx.is_def_eq(type, mk_constant(get_string_name()))) diff --git a/src/library/comp_val.h b/src/library/comp_val.h index 7b338231cb..bd9e619765 100644 --- a/src/library/comp_val.h +++ b/src/library/comp_val.h @@ -37,19 +37,6 @@ optional mk_char_val_ne_proof(expr const & a, expr const & b); /* Similar to mk_nat_val_ne_proof, but for string type */ optional mk_string_val_ne_proof(expr a, expr b); -/* Return a proof for e >= 0 if e is a nonnegative int numeral. - - \pre typeof(e) is int. */ -optional mk_int_val_nonneg_proof(expr const & e); - -/* Return a proof for e > 0 if e is a nonnegative int numeral. - - \pre typeof(e) is int. */ -optional mk_int_val_pos_proof(expr const & a); - -/* Similar to mk_nat_val_ne_proof, but for int type */ -optional mk_int_val_ne_proof(expr const & a, expr const & b); - /* Return a proof for a != b, a/b has type nat/int/char/string, and they are distinct values. */ optional mk_val_ne_proof(type_context_old & ctx, expr const & a, expr const & b); diff --git a/src/library/constants.cpp b/src/library/constants.cpp index 8c038e2c27..639944ba2c 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -6,10 +6,6 @@ namespace lean{ name const * g_absurd = nullptr; name const * g_acc_cases_on = nullptr; name const * g_acc_rec = nullptr; -name const * g_add_comm_group = nullptr; -name const * g_add_comm_semigroup = nullptr; -name const * g_add_group = nullptr; -name const * g_add_monoid = nullptr; name const * g_and = nullptr; name const * g_and_elim_left = nullptr; name const * g_and_elim_right = nullptr; @@ -27,7 +23,6 @@ name const * g_bool_ff = nullptr; name const * g_bool_tt = nullptr; name const * g_combinator_K = nullptr; name const * g_cast = nullptr; -name const * g_cast_heq = nullptr; name const * g_char = nullptr; name const * g_char_mk = nullptr; name const * g_char_ne_of_vne = nullptr; @@ -44,7 +39,6 @@ name const * g_congr_arg = nullptr; name const * g_congr_fun = nullptr; name const * g_decidable = nullptr; name const * g_decidable_to_bool = nullptr; -name const * g_distrib = nullptr; name const * g_dite = nullptr; name const * g_empty = nullptr; name const * g_Exists = nullptr; @@ -59,43 +53,28 @@ name const * g_eq_subst = nullptr; name const * g_eq_symm = nullptr; name const * g_eq_trans = nullptr; name const * g_eq_of_heq = nullptr; -name const * g_eq_rec_heq = nullptr; name const * g_eq_true_intro = nullptr; name const * g_eq_false_intro = nullptr; name const * g_eq_self_iff_true = nullptr; name const * g_expr = nullptr; name const * g_expr_subst = nullptr; -name const * g_format = nullptr; name const * g_false = nullptr; name const * g_false_of_true_iff_false = nullptr; name const * g_false_of_true_eq_false = nullptr; -name const * g_true_eq_false_of_false = nullptr; name const * g_false_rec = nullptr; -name const * g_field = nullptr; name const * g_fin_mk = nullptr; name const * g_fin_ne_of_vne = nullptr; name const * g_forall_congr = nullptr; name const * g_forall_congr_eq = nullptr; -name const * g_forall_not_of_not_exists = nullptr; name const * g_funext = nullptr; name const * g_has_add = nullptr; name const * g_has_add_add = nullptr; name const * g_has_andthen_andthen = nullptr; name const * g_has_bind_and_then = nullptr; name const * g_has_bind_seq = nullptr; -name const * g_has_div = nullptr; name const * g_has_div_div = nullptr; name const * g_has_emptyc_emptyc = nullptr; -name const * g_has_mul = nullptr; -name const * g_has_mul_mul = nullptr; name const * g_has_insert_insert = nullptr; -name const * g_has_inv = nullptr; -name const * g_has_inv_inv = nullptr; -name const * g_has_le = nullptr; -name const * g_has_le_le = nullptr; -name const * g_has_lt = nullptr; -name const * g_has_lt_lt = nullptr; -name const * g_has_neg = nullptr; name const * g_has_neg_neg = nullptr; name const * g_has_one = nullptr; name const * g_has_one_one = nullptr; @@ -103,9 +82,7 @@ name const * g_has_orelse_orelse = nullptr; name const * g_has_sep_sep = nullptr; name const * g_has_sizeof = nullptr; name const * g_has_sizeof_mk = nullptr; -name const * g_has_sub = nullptr; name const * g_has_sub_sub = nullptr; -name const * g_has_to_format = nullptr; name const * g_has_repr = nullptr; name const * g_has_well_founded = nullptr; name const * g_has_well_founded_r = nullptr; @@ -118,7 +95,6 @@ name const * g_heq_refl = nullptr; name const * g_heq_symm = nullptr; name const * g_heq_trans = nullptr; name const * g_heq_of_eq = nullptr; -name const * g_hole_command = nullptr; name const * g_id = nullptr; name const * g_id_rhs = nullptr; name const * g_id_delta = nullptr; @@ -141,23 +117,6 @@ name const * g_implies = nullptr; name const * g_implies_of_if_neg = nullptr; name const * g_implies_of_if_pos = nullptr; name const * g_int = nullptr; -name const * g_int_bit0_nonneg = nullptr; -name const * g_int_bit1_nonneg = nullptr; -name const * g_int_one_nonneg = nullptr; -name const * g_int_zero_nonneg = nullptr; -name const * g_int_bit0_pos = nullptr; -name const * g_int_bit1_pos = nullptr; -name const * g_int_one_pos = nullptr; -name const * g_int_nat_abs_zero = nullptr; -name const * g_int_nat_abs_one = nullptr; -name const * g_int_nat_abs_bit0_step = nullptr; -name const * g_int_nat_abs_bit1_nonneg_step = nullptr; -name const * g_int_ne_of_nat_ne_nonneg_case = nullptr; -name const * g_int_ne_neg_of_ne = nullptr; -name const * g_int_neg_ne_of_pos = nullptr; -name const * g_int_ne_neg_of_pos = nullptr; -name const * g_int_neg_ne_zero_of_ne = nullptr; -name const * g_int_zero_ne_neg_of_ne = nullptr; name const * g_interactive_param_desc = nullptr; name const * g_interactive_parse = nullptr; name const * g_io_core = nullptr; @@ -167,31 +126,17 @@ name const * g_monad_io_file_system_impl = nullptr; name const * g_monad_io_environment_impl = nullptr; name const * g_monad_io_process_impl = nullptr; name const * g_monad_io_random_impl = nullptr; -name const * g_io_rand_nat = nullptr; name const * g_io = nullptr; -name const * g_is_associative = nullptr; -name const * g_is_associative_assoc = nullptr; -name const * g_is_commutative = nullptr; -name const * g_is_commutative_comm = nullptr; name const * g_ite = nullptr; name const * g_lean_parser = nullptr; name const * g_lean_parser_pexpr = nullptr; name const * g_lean_parser_tk = nullptr; -name const * g_left_distrib = nullptr; -name const * g_left_comm = nullptr; -name const * g_le_refl = nullptr; -name const * g_linear_ordered_ring = nullptr; -name const * g_linear_ordered_semiring = nullptr; name const * g_list = nullptr; name const * g_list_nil = nullptr; name const * g_list_cons = nullptr; name const * g_match_failed = nullptr; name const * g_monad = nullptr; name const * g_monad_fail = nullptr; -name const * g_monoid = nullptr; -name const * g_mul_one = nullptr; -name const * g_mul_zero = nullptr; -name const * g_mul_zero_class = nullptr; name const * g_name_anonymous = nullptr; name const * g_name_mk_numeral = nullptr; name const * g_name_mk_string = nullptr; @@ -230,53 +175,6 @@ name const * g_nat_le_of_lt = nullptr; name const * g_nat_le_refl = nullptr; name const * g_ne = nullptr; name const * g_neq_of_not_iff = nullptr; -name const * g_norm_num_add1 = nullptr; -name const * g_norm_num_add1_bit0 = nullptr; -name const * g_norm_num_add1_bit1_helper = nullptr; -name const * g_norm_num_add1_one = nullptr; -name const * g_norm_num_add1_zero = nullptr; -name const * g_norm_num_add_div_helper = nullptr; -name const * g_norm_num_bin_add_zero = nullptr; -name const * g_norm_num_bin_zero_add = nullptr; -name const * g_norm_num_bit0_add_bit0_helper = nullptr; -name const * g_norm_num_bit0_add_bit1_helper = nullptr; -name const * g_norm_num_bit0_add_one = nullptr; -name const * g_norm_num_bit1_add_bit0_helper = nullptr; -name const * g_norm_num_bit1_add_bit1_helper = nullptr; -name const * g_norm_num_bit1_add_one_helper = nullptr; -name const * g_norm_num_div_add_helper = nullptr; -name const * g_norm_num_div_eq_div_helper = nullptr; -name const * g_norm_num_div_helper = nullptr; -name const * g_norm_num_div_mul_helper = nullptr; -name const * g_norm_num_mk_cong = nullptr; -name const * g_norm_num_mul_bit0_helper = nullptr; -name const * g_norm_num_mul_bit1_helper = nullptr; -name const * g_norm_num_mul_div_helper = nullptr; -name const * g_norm_num_neg_add_neg_helper = nullptr; -name const * g_norm_num_neg_add_pos_helper1 = nullptr; -name const * g_norm_num_neg_add_pos_helper2 = nullptr; -name const * g_norm_num_neg_mul_neg_helper = nullptr; -name const * g_norm_num_neg_mul_pos_helper = nullptr; -name const * g_norm_num_neg_neg_helper = nullptr; -name const * g_norm_num_neg_zero_helper = nullptr; -name const * g_norm_num_nonneg_bit0_helper = nullptr; -name const * g_norm_num_nonneg_bit1_helper = nullptr; -name const * g_norm_num_nonzero_of_div_helper = nullptr; -name const * g_norm_num_nonzero_of_neg_helper = nullptr; -name const * g_norm_num_nonzero_of_pos_helper = nullptr; -name const * g_norm_num_one_add_bit0 = nullptr; -name const * g_norm_num_one_add_bit1_helper = nullptr; -name const * g_norm_num_one_add_one = nullptr; -name const * g_norm_num_pos_add_neg_helper = nullptr; -name const * g_norm_num_pos_bit0_helper = nullptr; -name const * g_norm_num_pos_bit1_helper = nullptr; -name const * g_norm_num_pos_mul_neg_helper = nullptr; -name const * g_norm_num_sub_nat_zero_helper = nullptr; -name const * g_norm_num_sub_nat_pos_helper = nullptr; -name const * g_norm_num_subst_into_div = nullptr; -name const * g_norm_num_subst_into_prod = nullptr; -name const * g_norm_num_subst_into_subtr = nullptr; -name const * g_norm_num_subst_into_sum = nullptr; name const * g_not = nullptr; name const * g_not_of_iff_false = nullptr; name const * g_not_of_eq_false = nullptr; @@ -301,11 +199,8 @@ name const * g_reflected = nullptr; name const * g_reflected_subst = nullptr; name const * g_repr = nullptr; name const * g_rfl = nullptr; -name const * g_right_distrib = nullptr; -name const * g_ring = nullptr; name const * g_scope_trace = nullptr; name const * g_set_of = nullptr; -name const * g_semiring = nullptr; name const * g_psigma = nullptr; name const * g_psigma_cases_on = nullptr; name const * g_psigma_mk = nullptr; @@ -322,7 +217,6 @@ name const * g_string_str_ne_str_left = nullptr; name const * g_string_str_ne_str_right = nullptr; name const * g_subsingleton = nullptr; name const * g_subsingleton_elim = nullptr; -name const * g_subsingleton_helim = nullptr; name const * g_subtype = nullptr; name const * g_subtype_mk = nullptr; name const * g_subtype_val = nullptr; @@ -336,38 +230,26 @@ name const * g_tactic_try = nullptr; name const * g_tactic_triv = nullptr; name const * g_tactic_mk_inj_eq = nullptr; name const * g_thunk = nullptr; -name const * g_to_fmt = nullptr; name const * g_trans_rel_left = nullptr; name const * g_trans_rel_right = nullptr; name const * g_true = nullptr; name const * g_true_intro = nullptr; name const * g_typed_expr = nullptr; -name const * g_unification_hint = nullptr; -name const * g_unification_hint_mk = nullptr; name const * g_unit = nullptr; name const * g_unit_star = nullptr; name const * g_monad_from_pure_bind = nullptr; name const * g_user_attribute = nullptr; name const * g_user_attribute_parse_reflect = nullptr; -name const * g_vm_monitor = nullptr; -name const * g_partial_order = nullptr; name const * g_well_founded_fix = nullptr; name const * g_well_founded_fix_eq = nullptr; name const * g_well_founded_tactics = nullptr; name const * g_well_founded_tactics_default = nullptr; name const * g_well_founded_tactics_rel_tac = nullptr; name const * g_well_founded_tactics_dec_tac = nullptr; -name const * g_zero_le_one = nullptr; -name const * g_zero_lt_one = nullptr; -name const * g_zero_mul = nullptr; void initialize_constants() { g_absurd = new name{"absurd"}; g_acc_cases_on = new name{"acc", "cases_on"}; g_acc_rec = new name{"acc", "rec"}; - g_add_comm_group = new name{"add_comm_group"}; - g_add_comm_semigroup = new name{"add_comm_semigroup"}; - g_add_group = new name{"add_group"}; - g_add_monoid = new name{"add_monoid"}; g_and = new name{"and"}; g_and_elim_left = new name{"and", "elim_left"}; g_and_elim_right = new name{"and", "elim_right"}; @@ -385,7 +267,6 @@ void initialize_constants() { g_bool_tt = new name{"bool", "tt"}; g_combinator_K = new name{"combinator", "K"}; g_cast = new name{"cast"}; - g_cast_heq = new name{"cast_heq"}; g_char = new name{"char"}; g_char_mk = new name{"char", "mk"}; g_char_ne_of_vne = new name{"char", "ne_of_vne"}; @@ -402,7 +283,6 @@ void initialize_constants() { g_congr_fun = new name{"congr_fun"}; g_decidable = new name{"decidable"}; g_decidable_to_bool = new name{"decidable", "to_bool"}; - g_distrib = new name{"distrib"}; g_dite = new name{"dite"}; g_empty = new name{"empty"}; g_Exists = new name{"Exists"}; @@ -417,43 +297,28 @@ void initialize_constants() { g_eq_symm = new name{"eq", "symm"}; g_eq_trans = new name{"eq", "trans"}; g_eq_of_heq = new name{"eq_of_heq"}; - g_eq_rec_heq = new name{"eq_rec_heq"}; g_eq_true_intro = new name{"eq_true_intro"}; g_eq_false_intro = new name{"eq_false_intro"}; g_eq_self_iff_true = new name{"eq_self_iff_true"}; g_expr = new name{"expr"}; g_expr_subst = new name{"expr", "subst"}; - g_format = new name{"format"}; g_false = new name{"false"}; g_false_of_true_iff_false = new name{"false_of_true_iff_false"}; g_false_of_true_eq_false = new name{"false_of_true_eq_false"}; - g_true_eq_false_of_false = new name{"true_eq_false_of_false"}; g_false_rec = new name{"false", "rec"}; - g_field = new name{"field"}; g_fin_mk = new name{"fin", "mk"}; g_fin_ne_of_vne = new name{"fin", "ne_of_vne"}; g_forall_congr = new name{"forall_congr"}; g_forall_congr_eq = new name{"forall_congr_eq"}; - g_forall_not_of_not_exists = new name{"forall_not_of_not_exists"}; g_funext = new name{"funext"}; g_has_add = new name{"has_add"}; g_has_add_add = new name{"has_add", "add"}; g_has_andthen_andthen = new name{"has_andthen", "andthen"}; g_has_bind_and_then = new name{"has_bind", "and_then"}; g_has_bind_seq = new name{"has_bind", "seq"}; - g_has_div = new name{"has_div"}; g_has_div_div = new name{"has_div", "div"}; g_has_emptyc_emptyc = new name{"has_emptyc", "emptyc"}; - g_has_mul = new name{"has_mul"}; - g_has_mul_mul = new name{"has_mul", "mul"}; g_has_insert_insert = new name{"has_insert", "insert"}; - g_has_inv = new name{"has_inv"}; - g_has_inv_inv = new name{"has_inv", "inv"}; - g_has_le = new name{"has_le"}; - g_has_le_le = new name{"has_le", "le"}; - g_has_lt = new name{"has_lt"}; - g_has_lt_lt = new name{"has_lt", "lt"}; - g_has_neg = new name{"has_neg"}; g_has_neg_neg = new name{"has_neg", "neg"}; g_has_one = new name{"has_one"}; g_has_one_one = new name{"has_one", "one"}; @@ -461,9 +326,7 @@ void initialize_constants() { g_has_sep_sep = new name{"has_sep", "sep"}; g_has_sizeof = new name{"has_sizeof"}; g_has_sizeof_mk = new name{"has_sizeof", "mk"}; - g_has_sub = new name{"has_sub"}; g_has_sub_sub = new name{"has_sub", "sub"}; - g_has_to_format = new name{"has_to_format"}; g_has_repr = new name{"has_repr"}; g_has_well_founded = new name{"has_well_founded"}; g_has_well_founded_r = new name{"has_well_founded", "r"}; @@ -476,7 +339,6 @@ void initialize_constants() { g_heq_symm = new name{"heq", "symm"}; g_heq_trans = new name{"heq", "trans"}; g_heq_of_eq = new name{"heq_of_eq"}; - g_hole_command = new name{"hole_command"}; g_id = new name{"id"}; g_id_rhs = new name{"id_rhs"}; g_id_delta = new name{"id_delta"}; @@ -499,23 +361,6 @@ void initialize_constants() { g_implies_of_if_neg = new name{"implies_of_if_neg"}; g_implies_of_if_pos = new name{"implies_of_if_pos"}; g_int = new name{"int"}; - g_int_bit0_nonneg = new name{"int", "bit0_nonneg"}; - g_int_bit1_nonneg = new name{"int", "bit1_nonneg"}; - g_int_one_nonneg = new name{"int", "one_nonneg"}; - g_int_zero_nonneg = new name{"int", "zero_nonneg"}; - g_int_bit0_pos = new name{"int", "bit0_pos"}; - g_int_bit1_pos = new name{"int", "bit1_pos"}; - g_int_one_pos = new name{"int", "one_pos"}; - g_int_nat_abs_zero = new name{"int", "nat_abs_zero"}; - g_int_nat_abs_one = new name{"int", "nat_abs_one"}; - g_int_nat_abs_bit0_step = new name{"int", "nat_abs_bit0_step"}; - g_int_nat_abs_bit1_nonneg_step = new name{"int", "nat_abs_bit1_nonneg_step"}; - g_int_ne_of_nat_ne_nonneg_case = new name{"int", "ne_of_nat_ne_nonneg_case"}; - g_int_ne_neg_of_ne = new name{"int", "ne_neg_of_ne"}; - g_int_neg_ne_of_pos = new name{"int", "neg_ne_of_pos"}; - g_int_ne_neg_of_pos = new name{"int", "ne_neg_of_pos"}; - g_int_neg_ne_zero_of_ne = new name{"int", "neg_ne_zero_of_ne"}; - g_int_zero_ne_neg_of_ne = new name{"int", "zero_ne_neg_of_ne"}; g_interactive_param_desc = new name{"interactive", "param_desc"}; g_interactive_parse = new name{"interactive", "parse"}; g_io_core = new name{"io_core"}; @@ -525,31 +370,17 @@ void initialize_constants() { g_monad_io_environment_impl = new name{"monad_io_environment_impl"}; g_monad_io_process_impl = new name{"monad_io_process_impl"}; g_monad_io_random_impl = new name{"monad_io_random_impl"}; - g_io_rand_nat = new name{"io_rand_nat"}; g_io = new name{"io"}; - g_is_associative = new name{"is_associative"}; - g_is_associative_assoc = new name{"is_associative", "assoc"}; - g_is_commutative = new name{"is_commutative"}; - g_is_commutative_comm = new name{"is_commutative", "comm"}; g_ite = new name{"ite"}; g_lean_parser = new name{"lean", "parser"}; g_lean_parser_pexpr = new name{"lean", "parser", "pexpr"}; g_lean_parser_tk = new name{"lean", "parser", "tk"}; - g_left_distrib = new name{"left_distrib"}; - g_left_comm = new name{"left_comm"}; - g_le_refl = new name{"le_refl"}; - g_linear_ordered_ring = new name{"linear_ordered_ring"}; - g_linear_ordered_semiring = new name{"linear_ordered_semiring"}; g_list = new name{"list"}; g_list_nil = new name{"list", "nil"}; g_list_cons = new name{"list", "cons"}; g_match_failed = new name{"match_failed"}; g_monad = new name{"monad"}; g_monad_fail = new name{"monad_fail"}; - g_monoid = new name{"monoid"}; - g_mul_one = new name{"mul_one"}; - g_mul_zero = new name{"mul_zero"}; - g_mul_zero_class = new name{"mul_zero_class"}; g_name_anonymous = new name{"name", "anonymous"}; g_name_mk_numeral = new name{"name", "mk_numeral"}; g_name_mk_string = new name{"name", "mk_string"}; @@ -588,53 +419,6 @@ void initialize_constants() { g_nat_le_refl = new name{"nat", "le_refl"}; g_ne = new name{"ne"}; g_neq_of_not_iff = new name{"neq_of_not_iff"}; - g_norm_num_add1 = new name{"norm_num", "add1"}; - g_norm_num_add1_bit0 = new name{"norm_num", "add1_bit0"}; - g_norm_num_add1_bit1_helper = new name{"norm_num", "add1_bit1_helper"}; - g_norm_num_add1_one = new name{"norm_num", "add1_one"}; - g_norm_num_add1_zero = new name{"norm_num", "add1_zero"}; - g_norm_num_add_div_helper = new name{"norm_num", "add_div_helper"}; - g_norm_num_bin_add_zero = new name{"norm_num", "bin_add_zero"}; - g_norm_num_bin_zero_add = new name{"norm_num", "bin_zero_add"}; - g_norm_num_bit0_add_bit0_helper = new name{"norm_num", "bit0_add_bit0_helper"}; - g_norm_num_bit0_add_bit1_helper = new name{"norm_num", "bit0_add_bit1_helper"}; - g_norm_num_bit0_add_one = new name{"norm_num", "bit0_add_one"}; - g_norm_num_bit1_add_bit0_helper = new name{"norm_num", "bit1_add_bit0_helper"}; - g_norm_num_bit1_add_bit1_helper = new name{"norm_num", "bit1_add_bit1_helper"}; - g_norm_num_bit1_add_one_helper = new name{"norm_num", "bit1_add_one_helper"}; - g_norm_num_div_add_helper = new name{"norm_num", "div_add_helper"}; - g_norm_num_div_eq_div_helper = new name{"norm_num", "div_eq_div_helper"}; - g_norm_num_div_helper = new name{"norm_num", "div_helper"}; - g_norm_num_div_mul_helper = new name{"norm_num", "div_mul_helper"}; - g_norm_num_mk_cong = new name{"norm_num", "mk_cong"}; - g_norm_num_mul_bit0_helper = new name{"norm_num", "mul_bit0_helper"}; - g_norm_num_mul_bit1_helper = new name{"norm_num", "mul_bit1_helper"}; - g_norm_num_mul_div_helper = new name{"norm_num", "mul_div_helper"}; - g_norm_num_neg_add_neg_helper = new name{"norm_num", "neg_add_neg_helper"}; - g_norm_num_neg_add_pos_helper1 = new name{"norm_num", "neg_add_pos_helper1"}; - g_norm_num_neg_add_pos_helper2 = new name{"norm_num", "neg_add_pos_helper2"}; - g_norm_num_neg_mul_neg_helper = new name{"norm_num", "neg_mul_neg_helper"}; - g_norm_num_neg_mul_pos_helper = new name{"norm_num", "neg_mul_pos_helper"}; - g_norm_num_neg_neg_helper = new name{"norm_num", "neg_neg_helper"}; - g_norm_num_neg_zero_helper = new name{"norm_num", "neg_zero_helper"}; - g_norm_num_nonneg_bit0_helper = new name{"norm_num", "nonneg_bit0_helper"}; - g_norm_num_nonneg_bit1_helper = new name{"norm_num", "nonneg_bit1_helper"}; - g_norm_num_nonzero_of_div_helper = new name{"norm_num", "nonzero_of_div_helper"}; - g_norm_num_nonzero_of_neg_helper = new name{"norm_num", "nonzero_of_neg_helper"}; - g_norm_num_nonzero_of_pos_helper = new name{"norm_num", "nonzero_of_pos_helper"}; - g_norm_num_one_add_bit0 = new name{"norm_num", "one_add_bit0"}; - g_norm_num_one_add_bit1_helper = new name{"norm_num", "one_add_bit1_helper"}; - g_norm_num_one_add_one = new name{"norm_num", "one_add_one"}; - g_norm_num_pos_add_neg_helper = new name{"norm_num", "pos_add_neg_helper"}; - g_norm_num_pos_bit0_helper = new name{"norm_num", "pos_bit0_helper"}; - g_norm_num_pos_bit1_helper = new name{"norm_num", "pos_bit1_helper"}; - g_norm_num_pos_mul_neg_helper = new name{"norm_num", "pos_mul_neg_helper"}; - g_norm_num_sub_nat_zero_helper = new name{"norm_num", "sub_nat_zero_helper"}; - g_norm_num_sub_nat_pos_helper = new name{"norm_num", "sub_nat_pos_helper"}; - g_norm_num_subst_into_div = new name{"norm_num", "subst_into_div"}; - g_norm_num_subst_into_prod = new name{"norm_num", "subst_into_prod"}; - g_norm_num_subst_into_subtr = new name{"norm_num", "subst_into_subtr"}; - g_norm_num_subst_into_sum = new name{"norm_num", "subst_into_sum"}; g_not = new name{"not"}; g_not_of_iff_false = new name{"not_of_iff_false"}; g_not_of_eq_false = new name{"not_of_eq_false"}; @@ -659,11 +443,8 @@ void initialize_constants() { g_reflected_subst = new name{"reflected", "subst"}; g_repr = new name{"repr"}; g_rfl = new name{"rfl"}; - g_right_distrib = new name{"right_distrib"}; - g_ring = new name{"ring"}; g_scope_trace = new name{"scope_trace"}; g_set_of = new name{"set_of"}; - g_semiring = new name{"semiring"}; g_psigma = new name{"psigma"}; g_psigma_cases_on = new name{"psigma", "cases_on"}; g_psigma_mk = new name{"psigma", "mk"}; @@ -680,7 +461,6 @@ void initialize_constants() { g_string_str_ne_str_right = new name{"string", "str_ne_str_right"}; g_subsingleton = new name{"subsingleton"}; g_subsingleton_elim = new name{"subsingleton", "elim"}; - g_subsingleton_helim = new name{"subsingleton", "helim"}; g_subtype = new name{"subtype"}; g_subtype_mk = new name{"subtype", "mk"}; g_subtype_val = new name{"subtype", "val"}; @@ -694,39 +474,27 @@ void initialize_constants() { g_tactic_triv = new name{"tactic", "triv"}; g_tactic_mk_inj_eq = new name{"tactic", "mk_inj_eq"}; g_thunk = new name{"thunk"}; - g_to_fmt = new name{"to_fmt"}; g_trans_rel_left = new name{"trans_rel_left"}; g_trans_rel_right = new name{"trans_rel_right"}; g_true = new name{"true"}; g_true_intro = new name{"true", "intro"}; g_typed_expr = new name{"typed_expr"}; - g_unification_hint = new name{"unification_hint"}; - g_unification_hint_mk = new name{"unification_hint", "mk"}; g_unit = new name{"unit"}; g_unit_star = new name{"unit", "star"}; g_monad_from_pure_bind = new name{"monad_from_pure_bind"}; g_user_attribute = new name{"user_attribute"}; g_user_attribute_parse_reflect = new name{"user_attribute", "parse_reflect"}; - g_vm_monitor = new name{"vm_monitor"}; - g_partial_order = new name{"partial_order"}; g_well_founded_fix = new name{"well_founded", "fix"}; g_well_founded_fix_eq = new name{"well_founded", "fix_eq"}; g_well_founded_tactics = new name{"well_founded_tactics"}; g_well_founded_tactics_default = new name{"well_founded_tactics", "default"}; g_well_founded_tactics_rel_tac = new name{"well_founded_tactics", "rel_tac"}; g_well_founded_tactics_dec_tac = new name{"well_founded_tactics", "dec_tac"}; - g_zero_le_one = new name{"zero_le_one"}; - g_zero_lt_one = new name{"zero_lt_one"}; - g_zero_mul = new name{"zero_mul"}; } void finalize_constants() { delete g_absurd; delete g_acc_cases_on; delete g_acc_rec; - delete g_add_comm_group; - delete g_add_comm_semigroup; - delete g_add_group; - delete g_add_monoid; delete g_and; delete g_and_elim_left; delete g_and_elim_right; @@ -744,7 +512,6 @@ void finalize_constants() { delete g_bool_tt; delete g_combinator_K; delete g_cast; - delete g_cast_heq; delete g_char; delete g_char_mk; delete g_char_ne_of_vne; @@ -761,7 +528,6 @@ void finalize_constants() { delete g_congr_fun; delete g_decidable; delete g_decidable_to_bool; - delete g_distrib; delete g_dite; delete g_empty; delete g_Exists; @@ -776,43 +542,28 @@ void finalize_constants() { delete g_eq_symm; delete g_eq_trans; delete g_eq_of_heq; - delete g_eq_rec_heq; delete g_eq_true_intro; delete g_eq_false_intro; delete g_eq_self_iff_true; delete g_expr; delete g_expr_subst; - delete g_format; delete g_false; delete g_false_of_true_iff_false; delete g_false_of_true_eq_false; - delete g_true_eq_false_of_false; delete g_false_rec; - delete g_field; delete g_fin_mk; delete g_fin_ne_of_vne; delete g_forall_congr; delete g_forall_congr_eq; - delete g_forall_not_of_not_exists; delete g_funext; delete g_has_add; delete g_has_add_add; delete g_has_andthen_andthen; delete g_has_bind_and_then; delete g_has_bind_seq; - delete g_has_div; delete g_has_div_div; delete g_has_emptyc_emptyc; - delete g_has_mul; - delete g_has_mul_mul; delete g_has_insert_insert; - delete g_has_inv; - delete g_has_inv_inv; - delete g_has_le; - delete g_has_le_le; - delete g_has_lt; - delete g_has_lt_lt; - delete g_has_neg; delete g_has_neg_neg; delete g_has_one; delete g_has_one_one; @@ -820,9 +571,7 @@ void finalize_constants() { delete g_has_sep_sep; delete g_has_sizeof; delete g_has_sizeof_mk; - delete g_has_sub; delete g_has_sub_sub; - delete g_has_to_format; delete g_has_repr; delete g_has_well_founded; delete g_has_well_founded_r; @@ -835,7 +584,6 @@ void finalize_constants() { delete g_heq_symm; delete g_heq_trans; delete g_heq_of_eq; - delete g_hole_command; delete g_id; delete g_id_rhs; delete g_id_delta; @@ -858,23 +606,6 @@ void finalize_constants() { delete g_implies_of_if_neg; delete g_implies_of_if_pos; delete g_int; - delete g_int_bit0_nonneg; - delete g_int_bit1_nonneg; - delete g_int_one_nonneg; - delete g_int_zero_nonneg; - delete g_int_bit0_pos; - delete g_int_bit1_pos; - delete g_int_one_pos; - delete g_int_nat_abs_zero; - delete g_int_nat_abs_one; - delete g_int_nat_abs_bit0_step; - delete g_int_nat_abs_bit1_nonneg_step; - delete g_int_ne_of_nat_ne_nonneg_case; - delete g_int_ne_neg_of_ne; - delete g_int_neg_ne_of_pos; - delete g_int_ne_neg_of_pos; - delete g_int_neg_ne_zero_of_ne; - delete g_int_zero_ne_neg_of_ne; delete g_interactive_param_desc; delete g_interactive_parse; delete g_io_core; @@ -884,31 +615,17 @@ void finalize_constants() { delete g_monad_io_environment_impl; delete g_monad_io_process_impl; delete g_monad_io_random_impl; - delete g_io_rand_nat; delete g_io; - delete g_is_associative; - delete g_is_associative_assoc; - delete g_is_commutative; - delete g_is_commutative_comm; delete g_ite; delete g_lean_parser; delete g_lean_parser_pexpr; delete g_lean_parser_tk; - delete g_left_distrib; - delete g_left_comm; - delete g_le_refl; - delete g_linear_ordered_ring; - delete g_linear_ordered_semiring; delete g_list; delete g_list_nil; delete g_list_cons; delete g_match_failed; delete g_monad; delete g_monad_fail; - delete g_monoid; - delete g_mul_one; - delete g_mul_zero; - delete g_mul_zero_class; delete g_name_anonymous; delete g_name_mk_numeral; delete g_name_mk_string; @@ -947,53 +664,6 @@ void finalize_constants() { delete g_nat_le_refl; delete g_ne; delete g_neq_of_not_iff; - delete g_norm_num_add1; - delete g_norm_num_add1_bit0; - delete g_norm_num_add1_bit1_helper; - delete g_norm_num_add1_one; - delete g_norm_num_add1_zero; - delete g_norm_num_add_div_helper; - delete g_norm_num_bin_add_zero; - delete g_norm_num_bin_zero_add; - delete g_norm_num_bit0_add_bit0_helper; - delete g_norm_num_bit0_add_bit1_helper; - delete g_norm_num_bit0_add_one; - delete g_norm_num_bit1_add_bit0_helper; - delete g_norm_num_bit1_add_bit1_helper; - delete g_norm_num_bit1_add_one_helper; - delete g_norm_num_div_add_helper; - delete g_norm_num_div_eq_div_helper; - delete g_norm_num_div_helper; - delete g_norm_num_div_mul_helper; - delete g_norm_num_mk_cong; - delete g_norm_num_mul_bit0_helper; - delete g_norm_num_mul_bit1_helper; - delete g_norm_num_mul_div_helper; - delete g_norm_num_neg_add_neg_helper; - delete g_norm_num_neg_add_pos_helper1; - delete g_norm_num_neg_add_pos_helper2; - delete g_norm_num_neg_mul_neg_helper; - delete g_norm_num_neg_mul_pos_helper; - delete g_norm_num_neg_neg_helper; - delete g_norm_num_neg_zero_helper; - delete g_norm_num_nonneg_bit0_helper; - delete g_norm_num_nonneg_bit1_helper; - delete g_norm_num_nonzero_of_div_helper; - delete g_norm_num_nonzero_of_neg_helper; - delete g_norm_num_nonzero_of_pos_helper; - delete g_norm_num_one_add_bit0; - delete g_norm_num_one_add_bit1_helper; - delete g_norm_num_one_add_one; - delete g_norm_num_pos_add_neg_helper; - delete g_norm_num_pos_bit0_helper; - delete g_norm_num_pos_bit1_helper; - delete g_norm_num_pos_mul_neg_helper; - delete g_norm_num_sub_nat_zero_helper; - delete g_norm_num_sub_nat_pos_helper; - delete g_norm_num_subst_into_div; - delete g_norm_num_subst_into_prod; - delete g_norm_num_subst_into_subtr; - delete g_norm_num_subst_into_sum; delete g_not; delete g_not_of_iff_false; delete g_not_of_eq_false; @@ -1018,11 +688,8 @@ void finalize_constants() { delete g_reflected_subst; delete g_repr; delete g_rfl; - delete g_right_distrib; - delete g_ring; delete g_scope_trace; delete g_set_of; - delete g_semiring; delete g_psigma; delete g_psigma_cases_on; delete g_psigma_mk; @@ -1039,7 +706,6 @@ void finalize_constants() { delete g_string_str_ne_str_right; delete g_subsingleton; delete g_subsingleton_elim; - delete g_subsingleton_helim; delete g_subtype; delete g_subtype_mk; delete g_subtype_val; @@ -1053,38 +719,26 @@ void finalize_constants() { delete g_tactic_triv; delete g_tactic_mk_inj_eq; delete g_thunk; - delete g_to_fmt; delete g_trans_rel_left; delete g_trans_rel_right; delete g_true; delete g_true_intro; delete g_typed_expr; - delete g_unification_hint; - delete g_unification_hint_mk; delete g_unit; delete g_unit_star; delete g_monad_from_pure_bind; delete g_user_attribute; delete g_user_attribute_parse_reflect; - delete g_vm_monitor; - delete g_partial_order; delete g_well_founded_fix; delete g_well_founded_fix_eq; delete g_well_founded_tactics; delete g_well_founded_tactics_default; delete g_well_founded_tactics_rel_tac; delete g_well_founded_tactics_dec_tac; - delete g_zero_le_one; - delete g_zero_lt_one; - delete g_zero_mul; } name const & get_absurd_name() { return *g_absurd; } name const & get_acc_cases_on_name() { return *g_acc_cases_on; } name const & get_acc_rec_name() { return *g_acc_rec; } -name const & get_add_comm_group_name() { return *g_add_comm_group; } -name const & get_add_comm_semigroup_name() { return *g_add_comm_semigroup; } -name const & get_add_group_name() { return *g_add_group; } -name const & get_add_monoid_name() { return *g_add_monoid; } name const & get_and_name() { return *g_and; } name const & get_and_elim_left_name() { return *g_and_elim_left; } name const & get_and_elim_right_name() { return *g_and_elim_right; } @@ -1102,7 +756,6 @@ name const & get_bool_ff_name() { return *g_bool_ff; } name const & get_bool_tt_name() { return *g_bool_tt; } name const & get_combinator_K_name() { return *g_combinator_K; } name const & get_cast_name() { return *g_cast; } -name const & get_cast_heq_name() { return *g_cast_heq; } name const & get_char_name() { return *g_char; } name const & get_char_mk_name() { return *g_char_mk; } name const & get_char_ne_of_vne_name() { return *g_char_ne_of_vne; } @@ -1119,7 +772,6 @@ name const & get_congr_arg_name() { return *g_congr_arg; } name const & get_congr_fun_name() { return *g_congr_fun; } name const & get_decidable_name() { return *g_decidable; } name const & get_decidable_to_bool_name() { return *g_decidable_to_bool; } -name const & get_distrib_name() { return *g_distrib; } name const & get_dite_name() { return *g_dite; } name const & get_empty_name() { return *g_empty; } name const & get_Exists_name() { return *g_Exists; } @@ -1134,43 +786,28 @@ name const & get_eq_subst_name() { return *g_eq_subst; } name const & get_eq_symm_name() { return *g_eq_symm; } name const & get_eq_trans_name() { return *g_eq_trans; } name const & get_eq_of_heq_name() { return *g_eq_of_heq; } -name const & get_eq_rec_heq_name() { return *g_eq_rec_heq; } name const & get_eq_true_intro_name() { return *g_eq_true_intro; } name const & get_eq_false_intro_name() { return *g_eq_false_intro; } name const & get_eq_self_iff_true_name() { return *g_eq_self_iff_true; } name const & get_expr_name() { return *g_expr; } name const & get_expr_subst_name() { return *g_expr_subst; } -name const & get_format_name() { return *g_format; } name const & get_false_name() { return *g_false; } name const & get_false_of_true_iff_false_name() { return *g_false_of_true_iff_false; } name const & get_false_of_true_eq_false_name() { return *g_false_of_true_eq_false; } -name const & get_true_eq_false_of_false_name() { return *g_true_eq_false_of_false; } name const & get_false_rec_name() { return *g_false_rec; } -name const & get_field_name() { return *g_field; } name const & get_fin_mk_name() { return *g_fin_mk; } name const & get_fin_ne_of_vne_name() { return *g_fin_ne_of_vne; } name const & get_forall_congr_name() { return *g_forall_congr; } name const & get_forall_congr_eq_name() { return *g_forall_congr_eq; } -name const & get_forall_not_of_not_exists_name() { return *g_forall_not_of_not_exists; } name const & get_funext_name() { return *g_funext; } name const & get_has_add_name() { return *g_has_add; } name const & get_has_add_add_name() { return *g_has_add_add; } name const & get_has_andthen_andthen_name() { return *g_has_andthen_andthen; } name const & get_has_bind_and_then_name() { return *g_has_bind_and_then; } name const & get_has_bind_seq_name() { return *g_has_bind_seq; } -name const & get_has_div_name() { return *g_has_div; } name const & get_has_div_div_name() { return *g_has_div_div; } name const & get_has_emptyc_emptyc_name() { return *g_has_emptyc_emptyc; } -name const & get_has_mul_name() { return *g_has_mul; } -name const & get_has_mul_mul_name() { return *g_has_mul_mul; } name const & get_has_insert_insert_name() { return *g_has_insert_insert; } -name const & get_has_inv_name() { return *g_has_inv; } -name const & get_has_inv_inv_name() { return *g_has_inv_inv; } -name const & get_has_le_name() { return *g_has_le; } -name const & get_has_le_le_name() { return *g_has_le_le; } -name const & get_has_lt_name() { return *g_has_lt; } -name const & get_has_lt_lt_name() { return *g_has_lt_lt; } -name const & get_has_neg_name() { return *g_has_neg; } name const & get_has_neg_neg_name() { return *g_has_neg_neg; } name const & get_has_one_name() { return *g_has_one; } name const & get_has_one_one_name() { return *g_has_one_one; } @@ -1178,9 +815,7 @@ name const & get_has_orelse_orelse_name() { return *g_has_orelse_orelse; } name const & get_has_sep_sep_name() { return *g_has_sep_sep; } name const & get_has_sizeof_name() { return *g_has_sizeof; } name const & get_has_sizeof_mk_name() { return *g_has_sizeof_mk; } -name const & get_has_sub_name() { return *g_has_sub; } name const & get_has_sub_sub_name() { return *g_has_sub_sub; } -name const & get_has_to_format_name() { return *g_has_to_format; } name const & get_has_repr_name() { return *g_has_repr; } name const & get_has_well_founded_name() { return *g_has_well_founded; } name const & get_has_well_founded_r_name() { return *g_has_well_founded_r; } @@ -1193,7 +828,6 @@ name const & get_heq_refl_name() { return *g_heq_refl; } name const & get_heq_symm_name() { return *g_heq_symm; } name const & get_heq_trans_name() { return *g_heq_trans; } name const & get_heq_of_eq_name() { return *g_heq_of_eq; } -name const & get_hole_command_name() { return *g_hole_command; } name const & get_id_name() { return *g_id; } name const & get_id_rhs_name() { return *g_id_rhs; } name const & get_id_delta_name() { return *g_id_delta; } @@ -1216,23 +850,6 @@ name const & get_implies_name() { return *g_implies; } name const & get_implies_of_if_neg_name() { return *g_implies_of_if_neg; } name const & get_implies_of_if_pos_name() { return *g_implies_of_if_pos; } name const & get_int_name() { return *g_int; } -name const & get_int_bit0_nonneg_name() { return *g_int_bit0_nonneg; } -name const & get_int_bit1_nonneg_name() { return *g_int_bit1_nonneg; } -name const & get_int_one_nonneg_name() { return *g_int_one_nonneg; } -name const & get_int_zero_nonneg_name() { return *g_int_zero_nonneg; } -name const & get_int_bit0_pos_name() { return *g_int_bit0_pos; } -name const & get_int_bit1_pos_name() { return *g_int_bit1_pos; } -name const & get_int_one_pos_name() { return *g_int_one_pos; } -name const & get_int_nat_abs_zero_name() { return *g_int_nat_abs_zero; } -name const & get_int_nat_abs_one_name() { return *g_int_nat_abs_one; } -name const & get_int_nat_abs_bit0_step_name() { return *g_int_nat_abs_bit0_step; } -name const & get_int_nat_abs_bit1_nonneg_step_name() { return *g_int_nat_abs_bit1_nonneg_step; } -name const & get_int_ne_of_nat_ne_nonneg_case_name() { return *g_int_ne_of_nat_ne_nonneg_case; } -name const & get_int_ne_neg_of_ne_name() { return *g_int_ne_neg_of_ne; } -name const & get_int_neg_ne_of_pos_name() { return *g_int_neg_ne_of_pos; } -name const & get_int_ne_neg_of_pos_name() { return *g_int_ne_neg_of_pos; } -name const & get_int_neg_ne_zero_of_ne_name() { return *g_int_neg_ne_zero_of_ne; } -name const & get_int_zero_ne_neg_of_ne_name() { return *g_int_zero_ne_neg_of_ne; } name const & get_interactive_param_desc_name() { return *g_interactive_param_desc; } name const & get_interactive_parse_name() { return *g_interactive_parse; } name const & get_io_core_name() { return *g_io_core; } @@ -1242,31 +859,17 @@ name const & get_monad_io_file_system_impl_name() { return *g_monad_io_file_syst name const & get_monad_io_environment_impl_name() { return *g_monad_io_environment_impl; } name const & get_monad_io_process_impl_name() { return *g_monad_io_process_impl; } name const & get_monad_io_random_impl_name() { return *g_monad_io_random_impl; } -name const & get_io_rand_nat_name() { return *g_io_rand_nat; } name const & get_io_name() { return *g_io; } -name const & get_is_associative_name() { return *g_is_associative; } -name const & get_is_associative_assoc_name() { return *g_is_associative_assoc; } -name const & get_is_commutative_name() { return *g_is_commutative; } -name const & get_is_commutative_comm_name() { return *g_is_commutative_comm; } name const & get_ite_name() { return *g_ite; } name const & get_lean_parser_name() { return *g_lean_parser; } name const & get_lean_parser_pexpr_name() { return *g_lean_parser_pexpr; } name const & get_lean_parser_tk_name() { return *g_lean_parser_tk; } -name const & get_left_distrib_name() { return *g_left_distrib; } -name const & get_left_comm_name() { return *g_left_comm; } -name const & get_le_refl_name() { return *g_le_refl; } -name const & get_linear_ordered_ring_name() { return *g_linear_ordered_ring; } -name const & get_linear_ordered_semiring_name() { return *g_linear_ordered_semiring; } name const & get_list_name() { return *g_list; } name const & get_list_nil_name() { return *g_list_nil; } name const & get_list_cons_name() { return *g_list_cons; } name const & get_match_failed_name() { return *g_match_failed; } name const & get_monad_name() { return *g_monad; } name const & get_monad_fail_name() { return *g_monad_fail; } -name const & get_monoid_name() { return *g_monoid; } -name const & get_mul_one_name() { return *g_mul_one; } -name const & get_mul_zero_name() { return *g_mul_zero; } -name const & get_mul_zero_class_name() { return *g_mul_zero_class; } name const & get_name_anonymous_name() { return *g_name_anonymous; } name const & get_name_mk_numeral_name() { return *g_name_mk_numeral; } name const & get_name_mk_string_name() { return *g_name_mk_string; } @@ -1305,53 +908,6 @@ name const & get_nat_le_of_lt_name() { return *g_nat_le_of_lt; } name const & get_nat_le_refl_name() { return *g_nat_le_refl; } name const & get_ne_name() { return *g_ne; } name const & get_neq_of_not_iff_name() { return *g_neq_of_not_iff; } -name const & get_norm_num_add1_name() { return *g_norm_num_add1; } -name const & get_norm_num_add1_bit0_name() { return *g_norm_num_add1_bit0; } -name const & get_norm_num_add1_bit1_helper_name() { return *g_norm_num_add1_bit1_helper; } -name const & get_norm_num_add1_one_name() { return *g_norm_num_add1_one; } -name const & get_norm_num_add1_zero_name() { return *g_norm_num_add1_zero; } -name const & get_norm_num_add_div_helper_name() { return *g_norm_num_add_div_helper; } -name const & get_norm_num_bin_add_zero_name() { return *g_norm_num_bin_add_zero; } -name const & get_norm_num_bin_zero_add_name() { return *g_norm_num_bin_zero_add; } -name const & get_norm_num_bit0_add_bit0_helper_name() { return *g_norm_num_bit0_add_bit0_helper; } -name const & get_norm_num_bit0_add_bit1_helper_name() { return *g_norm_num_bit0_add_bit1_helper; } -name const & get_norm_num_bit0_add_one_name() { return *g_norm_num_bit0_add_one; } -name const & get_norm_num_bit1_add_bit0_helper_name() { return *g_norm_num_bit1_add_bit0_helper; } -name const & get_norm_num_bit1_add_bit1_helper_name() { return *g_norm_num_bit1_add_bit1_helper; } -name const & get_norm_num_bit1_add_one_helper_name() { return *g_norm_num_bit1_add_one_helper; } -name const & get_norm_num_div_add_helper_name() { return *g_norm_num_div_add_helper; } -name const & get_norm_num_div_eq_div_helper_name() { return *g_norm_num_div_eq_div_helper; } -name const & get_norm_num_div_helper_name() { return *g_norm_num_div_helper; } -name const & get_norm_num_div_mul_helper_name() { return *g_norm_num_div_mul_helper; } -name const & get_norm_num_mk_cong_name() { return *g_norm_num_mk_cong; } -name const & get_norm_num_mul_bit0_helper_name() { return *g_norm_num_mul_bit0_helper; } -name const & get_norm_num_mul_bit1_helper_name() { return *g_norm_num_mul_bit1_helper; } -name const & get_norm_num_mul_div_helper_name() { return *g_norm_num_mul_div_helper; } -name const & get_norm_num_neg_add_neg_helper_name() { return *g_norm_num_neg_add_neg_helper; } -name const & get_norm_num_neg_add_pos_helper1_name() { return *g_norm_num_neg_add_pos_helper1; } -name const & get_norm_num_neg_add_pos_helper2_name() { return *g_norm_num_neg_add_pos_helper2; } -name const & get_norm_num_neg_mul_neg_helper_name() { return *g_norm_num_neg_mul_neg_helper; } -name const & get_norm_num_neg_mul_pos_helper_name() { return *g_norm_num_neg_mul_pos_helper; } -name const & get_norm_num_neg_neg_helper_name() { return *g_norm_num_neg_neg_helper; } -name const & get_norm_num_neg_zero_helper_name() { return *g_norm_num_neg_zero_helper; } -name const & get_norm_num_nonneg_bit0_helper_name() { return *g_norm_num_nonneg_bit0_helper; } -name const & get_norm_num_nonneg_bit1_helper_name() { return *g_norm_num_nonneg_bit1_helper; } -name const & get_norm_num_nonzero_of_div_helper_name() { return *g_norm_num_nonzero_of_div_helper; } -name const & get_norm_num_nonzero_of_neg_helper_name() { return *g_norm_num_nonzero_of_neg_helper; } -name const & get_norm_num_nonzero_of_pos_helper_name() { return *g_norm_num_nonzero_of_pos_helper; } -name const & get_norm_num_one_add_bit0_name() { return *g_norm_num_one_add_bit0; } -name const & get_norm_num_one_add_bit1_helper_name() { return *g_norm_num_one_add_bit1_helper; } -name const & get_norm_num_one_add_one_name() { return *g_norm_num_one_add_one; } -name const & get_norm_num_pos_add_neg_helper_name() { return *g_norm_num_pos_add_neg_helper; } -name const & get_norm_num_pos_bit0_helper_name() { return *g_norm_num_pos_bit0_helper; } -name const & get_norm_num_pos_bit1_helper_name() { return *g_norm_num_pos_bit1_helper; } -name const & get_norm_num_pos_mul_neg_helper_name() { return *g_norm_num_pos_mul_neg_helper; } -name const & get_norm_num_sub_nat_zero_helper_name() { return *g_norm_num_sub_nat_zero_helper; } -name const & get_norm_num_sub_nat_pos_helper_name() { return *g_norm_num_sub_nat_pos_helper; } -name const & get_norm_num_subst_into_div_name() { return *g_norm_num_subst_into_div; } -name const & get_norm_num_subst_into_prod_name() { return *g_norm_num_subst_into_prod; } -name const & get_norm_num_subst_into_subtr_name() { return *g_norm_num_subst_into_subtr; } -name const & get_norm_num_subst_into_sum_name() { return *g_norm_num_subst_into_sum; } name const & get_not_name() { return *g_not; } name const & get_not_of_iff_false_name() { return *g_not_of_iff_false; } name const & get_not_of_eq_false_name() { return *g_not_of_eq_false; } @@ -1376,11 +932,8 @@ name const & get_reflected_name() { return *g_reflected; } name const & get_reflected_subst_name() { return *g_reflected_subst; } name const & get_repr_name() { return *g_repr; } name const & get_rfl_name() { return *g_rfl; } -name const & get_right_distrib_name() { return *g_right_distrib; } -name const & get_ring_name() { return *g_ring; } name const & get_scope_trace_name() { return *g_scope_trace; } name const & get_set_of_name() { return *g_set_of; } -name const & get_semiring_name() { return *g_semiring; } name const & get_psigma_name() { return *g_psigma; } name const & get_psigma_cases_on_name() { return *g_psigma_cases_on; } name const & get_psigma_mk_name() { return *g_psigma_mk; } @@ -1397,7 +950,6 @@ name const & get_string_str_ne_str_left_name() { return *g_string_str_ne_str_lef name const & get_string_str_ne_str_right_name() { return *g_string_str_ne_str_right; } name const & get_subsingleton_name() { return *g_subsingleton; } name const & get_subsingleton_elim_name() { return *g_subsingleton_elim; } -name const & get_subsingleton_helim_name() { return *g_subsingleton_helim; } name const & get_subtype_name() { return *g_subtype; } name const & get_subtype_mk_name() { return *g_subtype_mk; } name const & get_subtype_val_name() { return *g_subtype_val; } @@ -1411,28 +963,20 @@ name const & get_tactic_try_name() { return *g_tactic_try; } name const & get_tactic_triv_name() { return *g_tactic_triv; } name const & get_tactic_mk_inj_eq_name() { return *g_tactic_mk_inj_eq; } name const & get_thunk_name() { return *g_thunk; } -name const & get_to_fmt_name() { return *g_to_fmt; } name const & get_trans_rel_left_name() { return *g_trans_rel_left; } name const & get_trans_rel_right_name() { return *g_trans_rel_right; } name const & get_true_name() { return *g_true; } name const & get_true_intro_name() { return *g_true_intro; } name const & get_typed_expr_name() { return *g_typed_expr; } -name const & get_unification_hint_name() { return *g_unification_hint; } -name const & get_unification_hint_mk_name() { return *g_unification_hint_mk; } name const & get_unit_name() { return *g_unit; } name const & get_unit_star_name() { return *g_unit_star; } name const & get_monad_from_pure_bind_name() { return *g_monad_from_pure_bind; } name const & get_user_attribute_name() { return *g_user_attribute; } name const & get_user_attribute_parse_reflect_name() { return *g_user_attribute_parse_reflect; } -name const & get_vm_monitor_name() { return *g_vm_monitor; } -name const & get_partial_order_name() { return *g_partial_order; } name const & get_well_founded_fix_name() { return *g_well_founded_fix; } name const & get_well_founded_fix_eq_name() { return *g_well_founded_fix_eq; } name const & get_well_founded_tactics_name() { return *g_well_founded_tactics; } name const & get_well_founded_tactics_default_name() { return *g_well_founded_tactics_default; } name const & get_well_founded_tactics_rel_tac_name() { return *g_well_founded_tactics_rel_tac; } name const & get_well_founded_tactics_dec_tac_name() { return *g_well_founded_tactics_dec_tac; } -name const & get_zero_le_one_name() { return *g_zero_le_one; } -name const & get_zero_lt_one_name() { return *g_zero_lt_one; } -name const & get_zero_mul_name() { return *g_zero_mul; } } diff --git a/src/library/constants.h b/src/library/constants.h index 93dd41a09e..d3b6d2ac30 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -8,10 +8,6 @@ void finalize_constants(); name const & get_absurd_name(); name const & get_acc_cases_on_name(); name const & get_acc_rec_name(); -name const & get_add_comm_group_name(); -name const & get_add_comm_semigroup_name(); -name const & get_add_group_name(); -name const & get_add_monoid_name(); name const & get_and_name(); name const & get_and_elim_left_name(); name const & get_and_elim_right_name(); @@ -29,7 +25,6 @@ name const & get_bool_ff_name(); name const & get_bool_tt_name(); name const & get_combinator_K_name(); name const & get_cast_name(); -name const & get_cast_heq_name(); name const & get_char_name(); name const & get_char_mk_name(); name const & get_char_ne_of_vne_name(); @@ -46,7 +41,6 @@ name const & get_congr_arg_name(); name const & get_congr_fun_name(); name const & get_decidable_name(); name const & get_decidable_to_bool_name(); -name const & get_distrib_name(); name const & get_dite_name(); name const & get_empty_name(); name const & get_Exists_name(); @@ -61,43 +55,28 @@ name const & get_eq_subst_name(); name const & get_eq_symm_name(); name const & get_eq_trans_name(); name const & get_eq_of_heq_name(); -name const & get_eq_rec_heq_name(); name const & get_eq_true_intro_name(); name const & get_eq_false_intro_name(); name const & get_eq_self_iff_true_name(); name const & get_expr_name(); name const & get_expr_subst_name(); -name const & get_format_name(); name const & get_false_name(); name const & get_false_of_true_iff_false_name(); name const & get_false_of_true_eq_false_name(); -name const & get_true_eq_false_of_false_name(); name const & get_false_rec_name(); -name const & get_field_name(); name const & get_fin_mk_name(); name const & get_fin_ne_of_vne_name(); name const & get_forall_congr_name(); name const & get_forall_congr_eq_name(); -name const & get_forall_not_of_not_exists_name(); name const & get_funext_name(); name const & get_has_add_name(); name const & get_has_add_add_name(); name const & get_has_andthen_andthen_name(); name const & get_has_bind_and_then_name(); name const & get_has_bind_seq_name(); -name const & get_has_div_name(); name const & get_has_div_div_name(); name const & get_has_emptyc_emptyc_name(); -name const & get_has_mul_name(); -name const & get_has_mul_mul_name(); name const & get_has_insert_insert_name(); -name const & get_has_inv_name(); -name const & get_has_inv_inv_name(); -name const & get_has_le_name(); -name const & get_has_le_le_name(); -name const & get_has_lt_name(); -name const & get_has_lt_lt_name(); -name const & get_has_neg_name(); name const & get_has_neg_neg_name(); name const & get_has_one_name(); name const & get_has_one_one_name(); @@ -105,9 +84,7 @@ name const & get_has_orelse_orelse_name(); name const & get_has_sep_sep_name(); name const & get_has_sizeof_name(); name const & get_has_sizeof_mk_name(); -name const & get_has_sub_name(); name const & get_has_sub_sub_name(); -name const & get_has_to_format_name(); name const & get_has_repr_name(); name const & get_has_well_founded_name(); name const & get_has_well_founded_r_name(); @@ -120,7 +97,6 @@ name const & get_heq_refl_name(); name const & get_heq_symm_name(); name const & get_heq_trans_name(); name const & get_heq_of_eq_name(); -name const & get_hole_command_name(); name const & get_id_name(); name const & get_id_rhs_name(); name const & get_id_delta_name(); @@ -143,23 +119,6 @@ name const & get_implies_name(); name const & get_implies_of_if_neg_name(); name const & get_implies_of_if_pos_name(); name const & get_int_name(); -name const & get_int_bit0_nonneg_name(); -name const & get_int_bit1_nonneg_name(); -name const & get_int_one_nonneg_name(); -name const & get_int_zero_nonneg_name(); -name const & get_int_bit0_pos_name(); -name const & get_int_bit1_pos_name(); -name const & get_int_one_pos_name(); -name const & get_int_nat_abs_zero_name(); -name const & get_int_nat_abs_one_name(); -name const & get_int_nat_abs_bit0_step_name(); -name const & get_int_nat_abs_bit1_nonneg_step_name(); -name const & get_int_ne_of_nat_ne_nonneg_case_name(); -name const & get_int_ne_neg_of_ne_name(); -name const & get_int_neg_ne_of_pos_name(); -name const & get_int_ne_neg_of_pos_name(); -name const & get_int_neg_ne_zero_of_ne_name(); -name const & get_int_zero_ne_neg_of_ne_name(); name const & get_interactive_param_desc_name(); name const & get_interactive_parse_name(); name const & get_io_core_name(); @@ -169,31 +128,17 @@ name const & get_monad_io_file_system_impl_name(); name const & get_monad_io_environment_impl_name(); name const & get_monad_io_process_impl_name(); name const & get_monad_io_random_impl_name(); -name const & get_io_rand_nat_name(); name const & get_io_name(); -name const & get_is_associative_name(); -name const & get_is_associative_assoc_name(); -name const & get_is_commutative_name(); -name const & get_is_commutative_comm_name(); name const & get_ite_name(); name const & get_lean_parser_name(); name const & get_lean_parser_pexpr_name(); name const & get_lean_parser_tk_name(); -name const & get_left_distrib_name(); -name const & get_left_comm_name(); -name const & get_le_refl_name(); -name const & get_linear_ordered_ring_name(); -name const & get_linear_ordered_semiring_name(); name const & get_list_name(); name const & get_list_nil_name(); name const & get_list_cons_name(); name const & get_match_failed_name(); name const & get_monad_name(); name const & get_monad_fail_name(); -name const & get_monoid_name(); -name const & get_mul_one_name(); -name const & get_mul_zero_name(); -name const & get_mul_zero_class_name(); name const & get_name_anonymous_name(); name const & get_name_mk_numeral_name(); name const & get_name_mk_string_name(); @@ -232,53 +177,6 @@ name const & get_nat_le_of_lt_name(); name const & get_nat_le_refl_name(); name const & get_ne_name(); name const & get_neq_of_not_iff_name(); -name const & get_norm_num_add1_name(); -name const & get_norm_num_add1_bit0_name(); -name const & get_norm_num_add1_bit1_helper_name(); -name const & get_norm_num_add1_one_name(); -name const & get_norm_num_add1_zero_name(); -name const & get_norm_num_add_div_helper_name(); -name const & get_norm_num_bin_add_zero_name(); -name const & get_norm_num_bin_zero_add_name(); -name const & get_norm_num_bit0_add_bit0_helper_name(); -name const & get_norm_num_bit0_add_bit1_helper_name(); -name const & get_norm_num_bit0_add_one_name(); -name const & get_norm_num_bit1_add_bit0_helper_name(); -name const & get_norm_num_bit1_add_bit1_helper_name(); -name const & get_norm_num_bit1_add_one_helper_name(); -name const & get_norm_num_div_add_helper_name(); -name const & get_norm_num_div_eq_div_helper_name(); -name const & get_norm_num_div_helper_name(); -name const & get_norm_num_div_mul_helper_name(); -name const & get_norm_num_mk_cong_name(); -name const & get_norm_num_mul_bit0_helper_name(); -name const & get_norm_num_mul_bit1_helper_name(); -name const & get_norm_num_mul_div_helper_name(); -name const & get_norm_num_neg_add_neg_helper_name(); -name const & get_norm_num_neg_add_pos_helper1_name(); -name const & get_norm_num_neg_add_pos_helper2_name(); -name const & get_norm_num_neg_mul_neg_helper_name(); -name const & get_norm_num_neg_mul_pos_helper_name(); -name const & get_norm_num_neg_neg_helper_name(); -name const & get_norm_num_neg_zero_helper_name(); -name const & get_norm_num_nonneg_bit0_helper_name(); -name const & get_norm_num_nonneg_bit1_helper_name(); -name const & get_norm_num_nonzero_of_div_helper_name(); -name const & get_norm_num_nonzero_of_neg_helper_name(); -name const & get_norm_num_nonzero_of_pos_helper_name(); -name const & get_norm_num_one_add_bit0_name(); -name const & get_norm_num_one_add_bit1_helper_name(); -name const & get_norm_num_one_add_one_name(); -name const & get_norm_num_pos_add_neg_helper_name(); -name const & get_norm_num_pos_bit0_helper_name(); -name const & get_norm_num_pos_bit1_helper_name(); -name const & get_norm_num_pos_mul_neg_helper_name(); -name const & get_norm_num_sub_nat_zero_helper_name(); -name const & get_norm_num_sub_nat_pos_helper_name(); -name const & get_norm_num_subst_into_div_name(); -name const & get_norm_num_subst_into_prod_name(); -name const & get_norm_num_subst_into_subtr_name(); -name const & get_norm_num_subst_into_sum_name(); name const & get_not_name(); name const & get_not_of_iff_false_name(); name const & get_not_of_eq_false_name(); @@ -303,11 +201,8 @@ name const & get_reflected_name(); name const & get_reflected_subst_name(); name const & get_repr_name(); name const & get_rfl_name(); -name const & get_right_distrib_name(); -name const & get_ring_name(); name const & get_scope_trace_name(); name const & get_set_of_name(); -name const & get_semiring_name(); name const & get_psigma_name(); name const & get_psigma_cases_on_name(); name const & get_psigma_mk_name(); @@ -324,7 +219,6 @@ name const & get_string_str_ne_str_left_name(); name const & get_string_str_ne_str_right_name(); name const & get_subsingleton_name(); name const & get_subsingleton_elim_name(); -name const & get_subsingleton_helim_name(); name const & get_subtype_name(); name const & get_subtype_mk_name(); name const & get_subtype_val_name(); @@ -338,28 +232,20 @@ name const & get_tactic_try_name(); name const & get_tactic_triv_name(); name const & get_tactic_mk_inj_eq_name(); name const & get_thunk_name(); -name const & get_to_fmt_name(); name const & get_trans_rel_left_name(); name const & get_trans_rel_right_name(); name const & get_true_name(); name const & get_true_intro_name(); name const & get_typed_expr_name(); -name const & get_unification_hint_name(); -name const & get_unification_hint_mk_name(); name const & get_unit_name(); name const & get_unit_star_name(); name const & get_monad_from_pure_bind_name(); name const & get_user_attribute_name(); name const & get_user_attribute_parse_reflect_name(); -name const & get_vm_monitor_name(); -name const & get_partial_order_name(); name const & get_well_founded_fix_name(); name const & get_well_founded_fix_eq_name(); name const & get_well_founded_tactics_name(); name const & get_well_founded_tactics_default_name(); name const & get_well_founded_tactics_rel_tac_name(); name const & get_well_founded_tactics_dec_tac_name(); -name const & get_zero_le_one_name(); -name const & get_zero_lt_one_name(); -name const & get_zero_mul_name(); } diff --git a/src/library/constants.txt b/src/library/constants.txt index ef8a368f86..0a3a6530cc 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -1,10 +1,6 @@ absurd acc.cases_on acc.rec -add_comm_group -add_comm_semigroup -add_group -add_monoid and and.elim_left and.elim_right @@ -22,7 +18,6 @@ bool.ff bool.tt combinator.K cast -cast_heq char char.mk char.ne_of_vne @@ -39,7 +34,6 @@ congr_arg congr_fun decidable decidable.to_bool -distrib dite empty Exists @@ -54,43 +48,28 @@ eq.subst eq.symm eq.trans eq_of_heq -eq_rec_heq eq_true_intro eq_false_intro eq_self_iff_true expr expr.subst -format false false_of_true_iff_false false_of_true_eq_false -true_eq_false_of_false false.rec -field fin.mk fin.ne_of_vne forall_congr forall_congr_eq -forall_not_of_not_exists funext has_add has_add.add has_andthen.andthen has_bind.and_then has_bind.seq -has_div has_div.div has_emptyc.emptyc -has_mul -has_mul.mul has_insert.insert -has_inv -has_inv.inv -has_le -has_le.le -has_lt -has_lt.lt -has_neg has_neg.neg has_one has_one.one @@ -98,9 +77,7 @@ has_orelse.orelse has_sep.sep has_sizeof has_sizeof.mk -has_sub has_sub.sub -has_to_format has_repr has_well_founded has_well_founded.r @@ -113,7 +90,6 @@ heq.refl heq.symm heq.trans heq_of_eq -hole_command id id_rhs id_delta @@ -136,23 +112,6 @@ implies implies_of_if_neg implies_of_if_pos int -int.bit0_nonneg -int.bit1_nonneg -int.one_nonneg -int.zero_nonneg -int.bit0_pos -int.bit1_pos -int.one_pos -int.nat_abs_zero -int.nat_abs_one -int.nat_abs_bit0_step -int.nat_abs_bit1_nonneg_step -int.ne_of_nat_ne_nonneg_case -int.ne_neg_of_ne -int.neg_ne_of_pos -int.ne_neg_of_pos -int.neg_ne_zero_of_ne -int.zero_ne_neg_of_ne interactive.param_desc interactive.parse io_core @@ -162,31 +121,17 @@ monad_io_file_system_impl monad_io_environment_impl monad_io_process_impl monad_io_random_impl -io_rand_nat io -is_associative -is_associative.assoc -is_commutative -is_commutative.comm ite lean.parser lean.parser.pexpr lean.parser.tk -left_distrib -left_comm -le_refl -linear_ordered_ring -linear_ordered_semiring list list.nil list.cons match_failed monad monad_fail -monoid -mul_one -mul_zero -mul_zero_class name.anonymous name.mk_numeral name.mk_string @@ -225,53 +170,6 @@ nat.le_of_lt nat.le_refl ne neq_of_not_iff -norm_num.add1 -norm_num.add1_bit0 -norm_num.add1_bit1_helper -norm_num.add1_one -norm_num.add1_zero -norm_num.add_div_helper -norm_num.bin_add_zero -norm_num.bin_zero_add -norm_num.bit0_add_bit0_helper -norm_num.bit0_add_bit1_helper -norm_num.bit0_add_one -norm_num.bit1_add_bit0_helper -norm_num.bit1_add_bit1_helper -norm_num.bit1_add_one_helper -norm_num.div_add_helper -norm_num.div_eq_div_helper -norm_num.div_helper -norm_num.div_mul_helper -norm_num.mk_cong -norm_num.mul_bit0_helper -norm_num.mul_bit1_helper -norm_num.mul_div_helper -norm_num.neg_add_neg_helper -norm_num.neg_add_pos_helper1 -norm_num.neg_add_pos_helper2 -norm_num.neg_mul_neg_helper -norm_num.neg_mul_pos_helper -norm_num.neg_neg_helper -norm_num.neg_zero_helper -norm_num.nonneg_bit0_helper -norm_num.nonneg_bit1_helper -norm_num.nonzero_of_div_helper -norm_num.nonzero_of_neg_helper -norm_num.nonzero_of_pos_helper -norm_num.one_add_bit0 -norm_num.one_add_bit1_helper -norm_num.one_add_one -norm_num.pos_add_neg_helper -norm_num.pos_bit0_helper -norm_num.pos_bit1_helper -norm_num.pos_mul_neg_helper -norm_num.sub_nat_zero_helper -norm_num.sub_nat_pos_helper -norm_num.subst_into_div -norm_num.subst_into_prod -norm_num.subst_into_subtr -norm_num.subst_into_sum not not_of_iff_false not_of_eq_false @@ -296,11 +194,8 @@ reflected reflected.subst repr rfl -right_distrib -ring scope_trace set_of -semiring psigma psigma.cases_on psigma.mk @@ -317,7 +212,6 @@ string.str_ne_str_left string.str_ne_str_right subsingleton subsingleton.elim -subsingleton.helim subtype subtype.mk subtype.val @@ -331,27 +225,19 @@ tactic.try tactic.triv tactic.mk_inj_eq thunk -to_fmt trans_rel_left trans_rel_right true true.intro typed_expr -unification_hint -unification_hint.mk unit unit.star monad_from_pure_bind user_attribute user_attribute.parse_reflect -vm_monitor -partial_order well_founded.fix well_founded.fix_eq well_founded_tactics well_founded_tactics.default well_founded_tactics.rel_tac well_founded_tactics.dec_tac -zero_le_one -zero_lt_one -zero_mul diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp index 6f9e65d1c5..a1fac4a4ab 100644 --- a/src/library/vm/vm.cpp +++ b/src/library/vm/vm.cpp @@ -3592,13 +3592,6 @@ unsigned get_vm_builtin_arity(name const & fn) { lean_unreachable(); } -environment vm_monitor_register(environment const & env, name const & d) { - expr const & type = env.get(d).get_type(); - if (!is_app_of(type, get_vm_monitor_name(), 1)) - throw exception("invalid vm_monitor.register argument, must be name of a definition of type (vm_monitor ?s) "); - return module::add_and_perform(env, std::make_shared(d)); -} - [[noreturn]] void vm_check_failed(char const * condition) { throw exception(sstream() << "vm check failed: " << condition << " (possibly due to incorrect axioms, or sorry)"); diff --git a/src/library/vm/vm.h b/src/library/vm/vm.h index a708d5744f..008a8e3be6 100644 --- a/src/library/vm/vm.h +++ b/src/library/vm/vm.h @@ -976,8 +976,6 @@ vm_obj invoke(unsigned fn_idx, vm_obj const & arg); void display_vm_code(std::ostream & out, unsigned code_sz, vm_instr const * code); -environment vm_monitor_register(environment const & env, name const & d); - void initialize_vm_core(); void finalize_vm_core(); diff --git a/src/library/vm/vm_expr.cpp b/src/library/vm/vm_expr.cpp index 1b7812c807..1822e0d8bc 100644 --- a/src/library/vm/vm_expr.cpp +++ b/src/library/vm/vm_expr.cpp @@ -416,10 +416,6 @@ vm_obj vm_mk_string_val_ne_proof(vm_obj const & a, vm_obj const & b) { return to_obj(mk_string_val_ne_proof(to_expr(a), to_expr(b))); } -vm_obj vm_mk_int_val_ne_proof(vm_obj const & a, vm_obj const & b) { - return to_obj(mk_int_val_ne_proof(to_expr(a), to_expr(b))); -} - vm_obj expr_mk_sorry(vm_obj const & t) { return to_obj(mk_sorry(to_expr(t))); } @@ -522,7 +518,6 @@ void initialize_vm_expr() { DECLARE_VM_BUILTIN(name("mk_fin_val_ne_proof"), vm_mk_fin_val_ne_proof); DECLARE_VM_BUILTIN(name("mk_char_val_ne_proof"), vm_mk_char_val_ne_proof); DECLARE_VM_BUILTIN(name("mk_string_val_ne_proof"), vm_mk_string_val_ne_proof); - DECLARE_VM_BUILTIN(name("mk_int_val_ne_proof"), vm_mk_int_val_ne_proof); DECLARE_VM_BUILTIN(name("expr", "is_annotation"), expr_is_annotation); diff --git a/src/library/vm/vm_io.cpp b/src/library/vm/vm_io.cpp index 35772428ae..250433e6a0 100644 --- a/src/library/vm/vm_io.cpp +++ b/src/library/vm/vm_io.cpp @@ -562,10 +562,7 @@ vm_obj io_rand(vm_obj const & lo, vm_obj const & hi, vm_obj const &) { } return mk_io_result(mk_vm_nat(r)); } else { - vm_obj io_rand_nat = get_vm_state().get_constant(get_io_rand_nat_name()); - vm_obj r = invoke(io_rand_nat, gen, lo, hi); - gen = cfield(r, 1); - return mk_io_result(cfield(r, 0)); + return mk_io_failure("not implemented yet, io_rand_nat primitive has been deleted"); } } diff --git a/tests/lean/run/check_constants.lean b/tests/lean/run/check_constants.lean new file mode 100644 index 0000000000..74e16bce55 --- /dev/null +++ b/tests/lean/run/check_constants.lean @@ -0,0 +1,248 @@ +-- DO NOT EDIT, automatically generated file, generator scripts/gen_constants_cpp.py +import system.io +open tactic +meta def script_check_id (n : name) : tactic unit := +do env ← get_env, (env^.get n >> return ()) <|> (guard $ env^.is_namespace n) <|> (attribute.get_instances n >> return ()) <|> fail ("identifier '" ++ to_string n ++ "' is not a constant, namespace nor attribute") +run_cmd script_check_id `absurd +run_cmd script_check_id `acc.cases_on +run_cmd script_check_id `acc.rec +run_cmd script_check_id `and +run_cmd script_check_id `and.elim_left +run_cmd script_check_id `and.elim_right +run_cmd script_check_id `and.intro +run_cmd script_check_id `and.rec +run_cmd script_check_id `and.cases_on +run_cmd script_check_id `auto_param +run_cmd script_check_id `bit0 +run_cmd script_check_id `bit1 +run_cmd script_check_id `bin_tree.empty +run_cmd script_check_id `bin_tree.leaf +run_cmd script_check_id `bin_tree.node +run_cmd script_check_id `bool +run_cmd script_check_id `bool.ff +run_cmd script_check_id `bool.tt +run_cmd script_check_id `combinator.K +run_cmd script_check_id `cast +run_cmd script_check_id `char +run_cmd script_check_id `char.mk +run_cmd script_check_id `char.ne_of_vne +run_cmd script_check_id `char.of_nat +run_cmd script_check_id `char.of_nat_ne_of_ne +run_cmd script_check_id `is_valid_char_range_1 +run_cmd script_check_id `is_valid_char_range_2 +run_cmd script_check_id `coe +run_cmd script_check_id `coe_fn +run_cmd script_check_id `coe_sort +run_cmd script_check_id `coe_to_lift +run_cmd script_check_id `congr +run_cmd script_check_id `congr_arg +run_cmd script_check_id `congr_fun +run_cmd script_check_id `decidable +run_cmd script_check_id `decidable.to_bool +run_cmd script_check_id `dite +run_cmd script_check_id `empty +run_cmd script_check_id `Exists +run_cmd script_check_id `eq +run_cmd script_check_id `eq.cases_on +run_cmd script_check_id `eq.drec +run_cmd script_check_id `eq.mp +run_cmd script_check_id `eq.mpr +run_cmd script_check_id `eq.rec +run_cmd script_check_id `eq.refl +run_cmd script_check_id `eq.subst +run_cmd script_check_id `eq.symm +run_cmd script_check_id `eq.trans +run_cmd script_check_id `eq_of_heq +run_cmd script_check_id `eq_true_intro +run_cmd script_check_id `eq_false_intro +run_cmd script_check_id `eq_self_iff_true +run_cmd script_check_id `expr +run_cmd script_check_id `expr.subst +run_cmd script_check_id `false +run_cmd script_check_id `false_of_true_iff_false +run_cmd script_check_id `false_of_true_eq_false +run_cmd script_check_id `false.rec +run_cmd script_check_id `fin.mk +run_cmd script_check_id `fin.ne_of_vne +run_cmd script_check_id `forall_congr +run_cmd script_check_id `forall_congr_eq +run_cmd script_check_id `funext +run_cmd script_check_id `has_add +run_cmd script_check_id `has_add.add +run_cmd script_check_id `has_andthen.andthen +run_cmd script_check_id `has_bind.and_then +run_cmd script_check_id `has_bind.seq +run_cmd script_check_id `has_div.div +run_cmd script_check_id `has_emptyc.emptyc +run_cmd script_check_id `has_insert.insert +run_cmd script_check_id `has_neg.neg +run_cmd script_check_id `has_one +run_cmd script_check_id `has_one.one +run_cmd script_check_id `has_orelse.orelse +run_cmd script_check_id `has_sep.sep +run_cmd script_check_id `has_sizeof +run_cmd script_check_id `has_sizeof.mk +run_cmd script_check_id `has_sub.sub +run_cmd script_check_id `has_repr +run_cmd script_check_id `has_well_founded +run_cmd script_check_id `has_well_founded.r +run_cmd script_check_id `has_well_founded.wf +run_cmd script_check_id `has_zero +run_cmd script_check_id `has_zero.zero +run_cmd script_check_id `has_coe_t +run_cmd script_check_id `heq +run_cmd script_check_id `heq.refl +run_cmd script_check_id `heq.symm +run_cmd script_check_id `heq.trans +run_cmd script_check_id `heq_of_eq +run_cmd script_check_id `id +run_cmd script_check_id `id_rhs +run_cmd script_check_id `id_delta +run_cmd script_check_id `if_neg +run_cmd script_check_id `if_pos +run_cmd script_check_id `iff +run_cmd script_check_id `iff_false_intro +run_cmd script_check_id `iff.intro +run_cmd script_check_id `iff.mp +run_cmd script_check_id `iff.mpr +run_cmd script_check_id `iff.refl +run_cmd script_check_id `iff.symm +run_cmd script_check_id `iff.trans +run_cmd script_check_id `iff_true_intro +run_cmd script_check_id `imp_congr +run_cmd script_check_id `imp_congr_eq +run_cmd script_check_id `imp_congr_ctx +run_cmd script_check_id `imp_congr_ctx_eq +run_cmd script_check_id `implies +run_cmd script_check_id `implies_of_if_neg +run_cmd script_check_id `implies_of_if_pos +run_cmd script_check_id `int +run_cmd script_check_id `interactive.param_desc +run_cmd script_check_id `interactive.parse +run_cmd script_check_id `io_core +run_cmd script_check_id `monad_io_impl +run_cmd script_check_id `monad_io_terminal_impl +run_cmd script_check_id `monad_io_file_system_impl +run_cmd script_check_id `monad_io_environment_impl +run_cmd script_check_id `monad_io_process_impl +run_cmd script_check_id `monad_io_random_impl +run_cmd script_check_id `io +run_cmd script_check_id `ite +run_cmd script_check_id `lean.parser +run_cmd script_check_id `lean.parser.pexpr +run_cmd script_check_id `lean.parser.tk +run_cmd script_check_id `list +run_cmd script_check_id `list.nil +run_cmd script_check_id `list.cons +run_cmd script_check_id `match_failed +run_cmd script_check_id `monad +run_cmd script_check_id `monad_fail +run_cmd script_check_id `name.anonymous +run_cmd script_check_id `name.mk_numeral +run_cmd script_check_id `name.mk_string +run_cmd script_check_id `nat +run_cmd script_check_id `nat.succ +run_cmd script_check_id `nat.zero +run_cmd script_check_id `nat.has_zero +run_cmd script_check_id `nat.has_one +run_cmd script_check_id `nat.has_add +run_cmd script_check_id `nat.add +run_cmd script_check_id `nat.cases_on +run_cmd script_check_id `nat.bit0_ne +run_cmd script_check_id `nat.bit0_ne_bit1 +run_cmd script_check_id `nat.bit0_ne_zero +run_cmd script_check_id `nat.bit0_ne_one +run_cmd script_check_id `nat.bit1_ne +run_cmd script_check_id `nat.bit1_ne_bit0 +run_cmd script_check_id `nat.bit1_ne_zero +run_cmd script_check_id `nat.bit1_ne_one +run_cmd script_check_id `nat.zero_ne_one +run_cmd script_check_id `nat.zero_ne_bit0 +run_cmd script_check_id `nat.zero_ne_bit1 +run_cmd script_check_id `nat.one_ne_zero +run_cmd script_check_id `nat.one_ne_bit0 +run_cmd script_check_id `nat.one_ne_bit1 +run_cmd script_check_id `nat.bit0_lt +run_cmd script_check_id `nat.bit1_lt +run_cmd script_check_id `nat.bit0_lt_bit1 +run_cmd script_check_id `nat.bit1_lt_bit0 +run_cmd script_check_id `nat.zero_lt_one +run_cmd script_check_id `nat.zero_lt_bit1 +run_cmd script_check_id `nat.zero_lt_bit0 +run_cmd script_check_id `nat.one_lt_bit0 +run_cmd script_check_id `nat.one_lt_bit1 +run_cmd script_check_id `nat.le_of_lt +run_cmd script_check_id `nat.le_refl +run_cmd script_check_id `ne +run_cmd script_check_id `neq_of_not_iff +run_cmd script_check_id `not +run_cmd script_check_id `not_of_iff_false +run_cmd script_check_id `not_of_eq_false +run_cmd script_check_id `of_eq_true +run_cmd script_check_id `of_iff_true +run_cmd script_check_id `opt_param +run_cmd script_check_id `or +run_cmd script_check_id `out_param +run_cmd script_check_id `punit +run_cmd script_check_id `punit.cases_on +run_cmd script_check_id `punit.star +run_cmd script_check_id `prod.mk +run_cmd script_check_id `pprod +run_cmd script_check_id `pprod.mk +run_cmd script_check_id `pprod.fst +run_cmd script_check_id `pprod.snd +run_cmd script_check_id `propext +run_cmd script_check_id `to_pexpr +run_cmd script_check_id `quot.mk +run_cmd script_check_id `quot.lift +run_cmd script_check_id `reflected +run_cmd script_check_id `reflected.subst +run_cmd script_check_id `repr +run_cmd script_check_id `rfl +run_cmd script_check_id `scope_trace +run_cmd script_check_id `set_of +run_cmd script_check_id `psigma +run_cmd script_check_id `psigma.cases_on +run_cmd script_check_id `psigma.mk +run_cmd script_check_id `psigma.fst +run_cmd script_check_id `psigma.snd +run_cmd script_check_id `singleton +run_cmd script_check_id `sizeof +run_cmd script_check_id `string +run_cmd script_check_id `string.empty +run_cmd script_check_id `string.str +run_cmd script_check_id `string.empty_ne_str +run_cmd script_check_id `string.str_ne_empty +run_cmd script_check_id `string.str_ne_str_left +run_cmd script_check_id `string.str_ne_str_right +run_cmd script_check_id `subsingleton +run_cmd script_check_id `subsingleton.elim +run_cmd script_check_id `subtype +run_cmd script_check_id `subtype.mk +run_cmd script_check_id `subtype.val +run_cmd script_check_id `subtype.rec +run_cmd script_check_id `psum +run_cmd script_check_id `psum.cases_on +run_cmd script_check_id `psum.inl +run_cmd script_check_id `psum.inr +run_cmd script_check_id `tactic +run_cmd script_check_id `tactic.try +run_cmd script_check_id `tactic.triv +run_cmd script_check_id `tactic.mk_inj_eq +run_cmd script_check_id `thunk +run_cmd script_check_id `trans_rel_left +run_cmd script_check_id `trans_rel_right +run_cmd script_check_id `true +run_cmd script_check_id `true.intro +run_cmd script_check_id `typed_expr +run_cmd script_check_id `unit +run_cmd script_check_id `unit.star +run_cmd script_check_id `monad_from_pure_bind +run_cmd script_check_id `user_attribute +run_cmd script_check_id `user_attribute.parse_reflect +run_cmd script_check_id `well_founded.fix +run_cmd script_check_id `well_founded.fix_eq +run_cmd script_check_id `well_founded_tactics +run_cmd script_check_id `well_founded_tactics.default +run_cmd script_check_id `well_founded_tactics.rel_tac +run_cmd script_check_id `well_founded_tactics.dec_tac