chore(library/constants.txt): remove dead variables

script/gen_constants_cpp.py

@@ -85,6 +85,10 @@ def main(argv=None):
             f.write('name const & get_%s_name() { return *g_%s; }\n' % (c[0], c[0]))
         # end namespace
         f.write('}\n')
+    for c in constants:
+        cmd = ("cd .. && grep --silent --include=\"*.h\" --include=\"*.cpp\" --exclude=\".#*\" --exclude=\"constants.*\" -R \"get_%s_name\" *" % c[0])
+        if os.system(cmd) != 0:
+            print("Warning: generated function 'get_%s_name' is not used in the source code" % c[0])
     # TODO: enable test file again
     return 0
     with open(tst_file, 'w') as f:
@@ -95,10 +99,6 @@ def main(argv=None):
         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");
         for c in constants:
             f.write("run_cmd script_check_id `%s\n" % c[1])
-    for c in constants:
-        cmd = ("cd .. && grep --silent --include=\"*.h\" --include=\"*.cpp\" --exclude=\".#*\" --exclude=\"constants.*\" -R \"get_%s_name\" *" % c[0])
-        if os.system(cmd) != 0:
-            print("Warning: generated function 'get_%s_name' is not used in the source code" % c[0])
     print("done")
     return 0
 

src/frontends/lean/builtin_exprs.cpp

@@ -866,36 +866,6 @@ expr mk_annotation_with_pos(parser &, name const & a, expr const & e, pos_info c
     return save_pos(r, pos);
 }
 
-static expr mk_bin_tree(parser & p, buffer<expr> const & args, unsigned start, unsigned end, pos_info const & pos) {
-    lean_assert(start < end);
-    lean_assert(end <= args.size());
-    if (end == start+1)
-        return p.save_pos(mk_app(p.save_pos(mk_constant(get_bin_tree_leaf_name()), pos), args[start]), pos);
-    unsigned mid = (start + end)/2;
-    expr left  = mk_bin_tree(p, args, start, mid, pos);
-    expr right = mk_bin_tree(p, args, mid, end, pos);
-    return p.save_pos(mk_app(p.save_pos(mk_constant(get_bin_tree_node_name()), pos),
-                             left, right),
-                      pos);
-}
-
-
-static expr parse_bin_tree(parser & p, unsigned, expr const *, pos_info const & pos) {
-    buffer<expr> es;
-    while (!p.curr_is_token(get_rbracket_tk())) {
-        es.push_back(p.parse_expr());
-        if (!p.curr_is_token(get_comma_tk()))
-            break;
-        p.next();
-    }
-    p.check_token_next(get_rbracket_tk(), "invalid `#[...]`, `]` expected");
-    if (es.empty()) {
-        return p.save_pos(mk_constant(get_bin_tree_empty_name()), pos);
-    } else {
-        return mk_bin_tree(p, es, 0, es.size(), pos);
-    }
-}
-
 static expr parse_node(parser & p, unsigned, expr const *, pos_info const &) {
     name macro = p.check_id_next("identifier expected");
     std::function<buffer<expr>()> go;
@@ -990,7 +960,6 @@ parse_table init_nud_table() {
     r = r.add({transition(".(", mk_ext_action(parse_inaccessible))}, x0);
     r = r.add({transition("._", mk_ext_action(parse_atomic_inaccessible))}, x0);
     r = r.add({transition("`", mk_ext_action(parse_quoted_name))}, x0);
-    r = r.add({transition("#[", mk_ext_action(parse_bin_tree))}, x0);
     // r = r.add({transition("(:", Expr), transition(":)", mk_ext_action(parse_pattern))}, x0);
     r = r.add({transition("()", mk_ext_action(parse_unit))}, x0);
     r = r.add({transition("(::)", mk_ext_action(parse_lambda_cons))}, x0);

src/frontends/lean/token_table.cpp

@@ -86,7 +86,7 @@ void init_token_table(token_table & t) {
          {"```(", g_max_prec}, {"`[", g_max_prec}, {"`", g_max_prec},
          {"%%", g_max_prec}, {"()", g_max_prec}, {"(::)", g_max_prec}, {")", 0}, {"'", 0},
          {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec},
-         {"[", g_max_prec}, {"#[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0},
+         {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0},
          {"{!", g_max_prec}, {"!}", 0},
          {"Type", g_max_prec}, {"Type*", g_max_prec}, {"Sort", g_max_prec}, {"Sort*", g_max_prec},
          {"(:", g_max_prec}, {":)", 0}, {".(", g_max_prec}, {"._", g_max_prec},

src/library/constants.cpp

@@ -4,8 +4,6 @@
 #include "util/name.h"
 namespace lean{
 name const * g_absurd = nullptr;
-name const * g_acc_cases_on = nullptr;
-name const * g_acc_rec = nullptr;
 name const * g_and = nullptr;
 name const * g_and_left = nullptr;
 name const * g_and_right = nullptr;
@@ -16,21 +14,13 @@ name const * g_array = nullptr;
 name const * g_auto_param = nullptr;
 name const * g_bit0 = nullptr;
 name const * g_bit1 = nullptr;
-name const * g_bin_tree_empty = nullptr;
-name const * g_bin_tree_leaf = nullptr;
-name const * g_bin_tree_node = nullptr;
 name const * g_bool = nullptr;
 name const * g_bool_false = nullptr;
 name const * g_bool_true = nullptr;
-name const * g_combinator_k = nullptr;
 name const * g_cast = nullptr;
 name const * g_char = nullptr;
 name const * g_char_mk = nullptr;
-name const * g_char_ne_of_vne = nullptr;
 name const * g_char_of_nat = nullptr;
-name const * g_char_of_nat_ne_of_ne = nullptr;
-name const * g_is_valid_char_range1 = nullptr;
-name const * g_is_valid_char_range2 = nullptr;
 name const * g_coe = nullptr;
 name const * g_coe_fn = nullptr;
 name const * g_coe_sort = nullptr;
@@ -41,8 +31,6 @@ name const * g_congr_fun = nullptr;
 name const * g_decidable = nullptr;
 name const * g_decidable_cases_on = nullptr;
 name const * g_decidable_to_bool = nullptr;
-name const * g_decidable_is_true = nullptr;
-name const * g_decidable_is_false = nullptr;
 name const * g_dite = nullptr;
 name const * g_empty = nullptr;
 name const * g_exists = nullptr;
@@ -63,22 +51,15 @@ name const * g_eq_false_intro = nullptr;
 name const * g_eq_self_iff_true = nullptr;
 name const * g_lean_level = nullptr;
 name const * g_lean_expr = nullptr;
-name const * g_lean_expr_subst = 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_false_rec = nullptr;
 name const * g_false_cases_on = 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_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_div = nullptr;
 name const * g_has_emptyc_emptyc = nullptr;
 name const * g_has_eval = nullptr;
@@ -87,10 +68,7 @@ name const * g_has_insert_insert = nullptr;
 name const * g_has_neg_neg = nullptr;
 name const * g_has_one = nullptr;
 name const * g_has_one_one = nullptr;
-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_sub = nullptr;
 name const * g_has_repr = nullptr;
 name const * g_has_well_founded = nullptr;
@@ -107,38 +85,19 @@ name const * g_heq_of_eq = nullptr;
 name const * g_id = nullptr;
 name const * g_id_rhs = nullptr;
 name const * g_id_delta = nullptr;
-name const * g_if_neg = nullptr;
-name const * g_if_pos = nullptr;
-name const * g_iff = nullptr;
 name const * g_iff_false_intro = nullptr;
-name const * g_iff_intro = nullptr;
+name const * g_iff = nullptr;
 name const * g_iff_mp = nullptr;
 name const * g_iff_mpr = nullptr;
 name const * g_iff_refl = nullptr;
 name const * g_iff_symm = nullptr;
 name const * g_iff_trans = nullptr;
 name const * g_iff_true_intro = nullptr;
-name const * g_imp_congr = nullptr;
-name const * g_imp_congr_eq = nullptr;
-name const * g_imp_congr_ctx = nullptr;
-name const * g_imp_congr_ctx_eq = nullptr;
-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_nat_abs = nullptr;
 name const * g_int_lt = nullptr;
 name const * g_int_dec_lt = nullptr;
 name const * g_int_of_nat = nullptr;
-name const * g_int_neg_succ_of_nat = nullptr;
-name const * g_interactive_param_desc = nullptr;
-name const * g_interactive_parse = nullptr;
-name const * g_monad_io_impl = nullptr;
-name const * g_monad_io_terminal_impl = nullptr;
-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_inline = nullptr;
 name const * g_io = nullptr;
 name const * g_ite = nullptr;
@@ -154,11 +113,6 @@ name const * g_lean_name = nullptr;
 name const * g_lean_name_anonymous = nullptr;
 name const * g_lean_name_mk_numeral = nullptr;
 name const * g_lean_name_mk_string = nullptr;
-name const * g_lean_name_no_confusion = nullptr;
-name const * g_lean_name_mk_string_ne_mk_string_of_ne_prefix = nullptr;
-name const * g_lean_name_mk_string_ne_mk_string_of_ne_string = nullptr;
-name const * g_lean_name_mk_numeral_ne_mk_numeral_of_ne_prefix = nullptr;
-name const * g_lean_name_mk_numeral_ne_mk_numeral_of_ne_numeral = nullptr;
 name const * g_nat = nullptr;
 name const * g_nat_succ = nullptr;
 name const * g_nat_zero = nullptr;
@@ -166,38 +120,8 @@ name const * g_nat_has_zero = nullptr;
 name const * g_nat_has_one = nullptr;
 name const * g_nat_has_add = nullptr;
 name const * g_nat_add = nullptr;
-name const * g_nat_cases_on = nullptr;
-name const * g_nat_bit0_ne = nullptr;
-name const * g_nat_bit0_ne_bit1 = nullptr;
-name const * g_nat_bit0_ne_zero = nullptr;
-name const * g_nat_bit0_ne_one = nullptr;
-name const * g_nat_bit1_ne = nullptr;
-name const * g_nat_bit1_ne_bit0 = nullptr;
-name const * g_nat_bit1_ne_zero = nullptr;
-name const * g_nat_bit1_ne_one = nullptr;
-name const * g_nat_zero_ne_one = nullptr;
-name const * g_nat_zero_ne_bit0 = nullptr;
-name const * g_nat_zero_ne_bit1 = nullptr;
-name const * g_nat_one_ne_zero = nullptr;
-name const * g_nat_one_ne_bit0 = nullptr;
-name const * g_nat_one_ne_bit1 = nullptr;
-name const * g_nat_bit0_lt = nullptr;
-name const * g_nat_bit1_lt = nullptr;
-name const * g_nat_bit0_lt_bit1 = nullptr;
-name const * g_nat_bit1_lt_bit0 = nullptr;
-name const * g_nat_zero_lt_one = nullptr;
-name const * g_nat_zero_lt_bit1 = nullptr;
-name const * g_nat_zero_lt_bit0 = nullptr;
-name const * g_nat_one_lt_bit0 = nullptr;
-name const * g_nat_one_lt_bit1 = nullptr;
-name const * g_nat_le_of_lt = nullptr;
-name const * g_nat_le_refl = nullptr;
-name const * g_nat_decidable_lt = nullptr;
 name const * g_nat_dec_eq = nullptr;
-name const * g_nat_mul = nullptr;
 name const * g_nat_sub = nullptr;
-name const * g_nat_beq = nullptr;
-name const * g_nat_ble = nullptr;
 name const * g_ne = nullptr;
 name const * g_neq_of_not_iff = nullptr;
 name const * g_not = nullptr;
@@ -208,10 +132,7 @@ name const * g_of_iff_true = nullptr;
 name const * g_opt_param = nullptr;
 name const * g_or = nullptr;
 name const * g_out_param = nullptr;
-name const * g_pexpr = nullptr;
-name const * g_pexpr_subst = nullptr;
 name const * g_punit = nullptr;
-name const * g_punit_cases_on = nullptr;
 name const * g_punit_unit = nullptr;
 name const * g_prod_mk = nullptr;
 name const * g_pprod = nullptr;
@@ -219,67 +140,42 @@ name const * g_pprod_mk = nullptr;
 name const * g_pprod_fst = nullptr;
 name const * g_pprod_snd = nullptr;
 name const * g_propext = nullptr;
-name const * g_to_pexpr = nullptr;
 name const * g_quot_mk = nullptr;
 name const * g_quot_lift = nullptr;
-name const * g_reflected = nullptr;
-name const * g_reflected_subst = nullptr;
 name const * g_repr = nullptr;
 name const * g_rfl = nullptr;
 name const * g_scope_trace = nullptr;
 name const * g_set_of = nullptr;
 name const * g_psigma = nullptr;
-name const * g_psigma_cases_on = nullptr;
 name const * g_psigma_mk = nullptr;
 name const * g_psigma_fst = nullptr;
 name const * g_psigma_snd = nullptr;
 name const * g_singleton = nullptr;
-name const * g_sizeof = nullptr;
 name const * g_sorry_ax = nullptr;
 name const * g_string = nullptr;
-name const * g_string_decidable_eq = nullptr;
-name const * g_string_mk = nullptr;
 name const * g_string_data = nullptr;
 name const * g_string_empty = nullptr;
 name const * g_string_str = nullptr;
-name const * g_string_empty_ne_str = nullptr;
-name const * g_string_str_ne_empty = nullptr;
-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_subtype = nullptr;
-name const * g_subtype_mk = nullptr;
-name const * g_subtype_val = nullptr;
-name const * g_subtype_rec = nullptr;
 name const * g_psum = nullptr;
 name const * g_psum_cases_on = nullptr;
 name const * g_psum_inl = nullptr;
 name const * g_psum_inr = nullptr;
-name const * g_tactic = nullptr;
-name const * g_tactic_try = nullptr;
-name const * g_tactic_triv = nullptr;
-name const * g_tactic_mk_inj_eq = nullptr;
 name const * g_task = nullptr;
 name const * g_thunk = nullptr;
-name const * g_thunk_mk = 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_unit = nullptr;
 name const * g_unit_unit = nullptr;
-name const * g_monad_from_pure_bind = nullptr;
 name const * g_uint8 = nullptr;
 name const * g_uint16 = nullptr;
 name const * g_uint32 = nullptr;
 name const * g_uint64 = nullptr;
 name const * g_usize = nullptr;
-name const * g_user_attribute = nullptr;
-name const * g_user_attribute_parse_reflect = 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;
@@ -287,8 +183,6 @@ name const * g_well_founded_tactics_dec_tac = nullptr;
 name const * g_wf_term_hack = nullptr;
 void initialize_constants() {
     g_absurd = new name{"absurd"};
-    g_acc_cases_on = new name{"Acc", "casesOn"};
-    g_acc_rec = new name{"Acc", "rec"};
     g_and = new name{"And"};
     g_and_left = new name{"And", "left"};
     g_and_right = new name{"And", "right"};
@@ -299,21 +193,13 @@ void initialize_constants() {
     g_auto_param = new name{"autoParam"};
     g_bit0 = new name{"bit0"};
     g_bit1 = new name{"bit1"};
-    g_bin_tree_empty = new name{"BinTree", "Empty"};
-    g_bin_tree_leaf = new name{"BinTree", "leaf"};
-    g_bin_tree_node = new name{"BinTree", "Node"};
     g_bool = new name{"Bool"};
     g_bool_false = new name{"Bool", "false"};
     g_bool_true = new name{"Bool", "true"};
-    g_combinator_k = new name{"Combinator", "K"};
     g_cast = new name{"cast"};
     g_char = new name{"Char"};
     g_char_mk = new name{"Char", "mk"};
-    g_char_ne_of_vne = new name{"Char", "neOfVne"};
     g_char_of_nat = new name{"Char", "ofNat"};
-    g_char_of_nat_ne_of_ne = new name{"Char", "ofNatNeOfNe"};
-    g_is_valid_char_range1 = new name{"isValidCharRange1"};
-    g_is_valid_char_range2 = new name{"isValidCharRange2"};
     g_coe = new name{"coe"};
     g_coe_fn = new name{"coeFn"};
     g_coe_sort = new name{"coeSort"};
@@ -324,8 +210,6 @@ void initialize_constants() {
     g_decidable = new name{"Decidable"};
     g_decidable_cases_on = new name{"Decidable", "casesOn"};
     g_decidable_to_bool = new name{"Decidable", "toBool"};
-    g_decidable_is_true = new name{"Decidable", "isTrue"};
-    g_decidable_is_false = new name{"Decidable", "isFalse"};
     g_dite = new name{"dite"};
     g_empty = new name{"Empty"};
     g_exists = new name{"Exists"};
@@ -346,22 +230,15 @@ void initialize_constants() {
     g_eq_self_iff_true = new name{"eqSelfIffTrue"};
     g_lean_level = new name{"Lean", "Level"};
     g_lean_expr = new name{"Lean", "Expr"};
-    g_lean_expr_subst = new name{"Lean", "Expr", "subst"};
     g_false = new name{"False"};
     g_false_of_true_iff_false = new name{"falseOfTrueIffFalse"};
     g_false_of_true_eq_false = new name{"falseOfTrueEqFalse"};
     g_false_rec = new name{"False", "rec"};
     g_false_cases_on = new name{"False", "casesOn"};
     g_fin_mk = new name{"Fin", "mk"};
-    g_fin_ne_of_vne = new name{"Fin", "neOfVne"};
-    g_forall_congr = new name{"forallCongr"};
-    g_forall_congr_eq = new name{"forallCongrEq"};
     g_funext = new name{"funext"};
     g_has_add = new name{"HasAdd"};
     g_has_add_add = new name{"HasAdd", "add"};
-    g_has_andthen_andthen = new name{"HasAndthen", "andthen"};
-    g_has_bind_and_then = new name{"HasBind", "andThen"};
-    g_has_bind_seq = new name{"HasBind", "Seq"};
     g_has_div_div = new name{"HasDiv", "div"};
     g_has_emptyc_emptyc = new name{"HasEmptyc", "emptyc"};
     g_has_eval = new name{"HasEval"};
@@ -370,10 +247,7 @@ void initialize_constants() {
     g_has_neg_neg = new name{"HasNeg", "neg"};
     g_has_one = new name{"HasOne"};
     g_has_one_one = new name{"HasOne", "one"};
-    g_has_orelse_orelse = new name{"HasOrelse", "orelse"};
     g_has_sep_sep = new name{"HasSep", "sep"};
-    g_has_sizeof = new name{"HasSizeof"};
-    g_has_sizeof_mk = new name{"HasSizeof", "mk"};
     g_has_sub_sub = new name{"HasSub", "sub"};
     g_has_repr = new name{"HasRepr"};
     g_has_well_founded = new name{"HasWellFounded"};
@@ -390,38 +264,19 @@ void initialize_constants() {
     g_id = new name{"id"};
     g_id_rhs = new name{"idRhs"};
     g_id_delta = new name{"idDelta"};
-    g_if_neg = new name{"ifNeg"};
-    g_if_pos = new name{"ifPos"};
-    g_iff = new name{"Iff"};
     g_iff_false_intro = new name{"iffFalseIntro"};
-    g_iff_intro = new name{"Iff", "intro"};
+    g_iff = new name{"Iff"};
     g_iff_mp = new name{"Iff", "mp"};
     g_iff_mpr = new name{"Iff", "mpr"};
     g_iff_refl = new name{"Iff", "refl"};
     g_iff_symm = new name{"Iff", "symm"};
     g_iff_trans = new name{"Iff", "trans"};
     g_iff_true_intro = new name{"iffTrueIntro"};
-    g_imp_congr = new name{"impCongr"};
-    g_imp_congr_eq = new name{"impCongrEq"};
-    g_imp_congr_ctx = new name{"impCongrCtx"};
-    g_imp_congr_ctx_eq = new name{"impCongrCtxEq"};
-    g_implies = new name{"implies"};
-    g_implies_of_if_neg = new name{"impliesOfIfNeg"};
-    g_implies_of_if_pos = new name{"impliesOfIfPos"};
     g_int = new name{"Int"};
     g_int_nat_abs = new name{"Int", "natAbs"};
     g_int_lt = new name{"Int", "lt"};
     g_int_dec_lt = new name{"Int", "decLt"};
     g_int_of_nat = new name{"Int", "ofNat"};
-    g_int_neg_succ_of_nat = new name{"Int", "negSuccOfNat"};
-    g_interactive_param_desc = new name{"interactive", "paramDesc"};
-    g_interactive_parse = new name{"interactive", "parse"};
-    g_monad_io_impl = new name{"monadIOImpl"};
-    g_monad_io_terminal_impl = new name{"monadIOTerminalImpl"};
-    g_monad_io_file_system_impl = new name{"monadIOFileSystemImpl"};
-    g_monad_io_environment_impl = new name{"monadIOEnvironmentImpl"};
-    g_monad_io_process_impl = new name{"monadIOProcessImpl"};
-    g_monad_io_random_impl = new name{"monadIORandomImpl"};
     g_inline = new name{"inline"};
     g_io = new name{"IO"};
     g_ite = new name{"ite"};
@@ -437,11 +292,6 @@ void initialize_constants() {
     g_lean_name_anonymous = new name{"Lean", "Name", "anonymous"};
     g_lean_name_mk_numeral = new name{"Lean", "Name", "mkNumeral"};
     g_lean_name_mk_string = new name{"Lean", "Name", "mkString"};
-    g_lean_name_no_confusion = new name{"Lean", "Name", "noConfusion"};
-    g_lean_name_mk_string_ne_mk_string_of_ne_prefix = new name{"Lean", "Name", "mkStringNeMkStringOfNePrefix"};
-    g_lean_name_mk_string_ne_mk_string_of_ne_string = new name{"Lean", "Name", "mkStringNeMkStringOfNeString"};
-    g_lean_name_mk_numeral_ne_mk_numeral_of_ne_prefix = new name{"Lean", "Name", "mkNumeralNeMkNumeralOfNePrefix"};
-    g_lean_name_mk_numeral_ne_mk_numeral_of_ne_numeral = new name{"Lean", "Name", "mkNumeralNeMkNumeralOfNeNumeral"};
     g_nat = new name{"Nat"};
     g_nat_succ = new name{"Nat", "succ"};
     g_nat_zero = new name{"Nat", "zero"};
@@ -449,38 +299,8 @@ void initialize_constants() {
     g_nat_has_one = new name{"Nat", "HasOne"};
     g_nat_has_add = new name{"Nat", "HasAdd"};
     g_nat_add = new name{"Nat", "add"};
-    g_nat_cases_on = new name{"Nat", "casesOn"};
-    g_nat_bit0_ne = new name{"Nat", "bit0Ne"};
-    g_nat_bit0_ne_bit1 = new name{"Nat", "bit0NeBit1"};
-    g_nat_bit0_ne_zero = new name{"Nat", "bit0NeZero"};
-    g_nat_bit0_ne_one = new name{"Nat", "bit0NeOne"};
-    g_nat_bit1_ne = new name{"Nat", "bit1Ne"};
-    g_nat_bit1_ne_bit0 = new name{"Nat", "bit1NeBit0"};
-    g_nat_bit1_ne_zero = new name{"Nat", "bit1NeZero"};
-    g_nat_bit1_ne_one = new name{"Nat", "bit1NeOne"};
-    g_nat_zero_ne_one = new name{"Nat", "zeroNeOne"};
-    g_nat_zero_ne_bit0 = new name{"Nat", "zeroNeBit0"};
-    g_nat_zero_ne_bit1 = new name{"Nat", "zeroNeBit1"};
-    g_nat_one_ne_zero = new name{"Nat", "oneNeZero"};
-    g_nat_one_ne_bit0 = new name{"Nat", "oneNeBit0"};
-    g_nat_one_ne_bit1 = new name{"Nat", "oneNeBit1"};
-    g_nat_bit0_lt = new name{"Nat", "bit0Lt"};
-    g_nat_bit1_lt = new name{"Nat", "bit1Lt"};
-    g_nat_bit0_lt_bit1 = new name{"Nat", "bit0LtBit1"};
-    g_nat_bit1_lt_bit0 = new name{"Nat", "bit1LtBit0"};
-    g_nat_zero_lt_one = new name{"Nat", "zeroLtOne"};
-    g_nat_zero_lt_bit1 = new name{"Nat", "zeroLtBit1"};
-    g_nat_zero_lt_bit0 = new name{"Nat", "zeroLtBit0"};
-    g_nat_one_lt_bit0 = new name{"Nat", "oneLtBit0"};
-    g_nat_one_lt_bit1 = new name{"Nat", "oneLtBit1"};
-    g_nat_le_of_lt = new name{"Nat", "leOfLt"};
-    g_nat_le_refl = new name{"Nat", "leRefl"};
-    g_nat_decidable_lt = new name{"Nat", "decidableLt"};
     g_nat_dec_eq = new name{"Nat", "decEq"};
-    g_nat_mul = new name{"Nat", "mul"};
     g_nat_sub = new name{"Nat", "sub"};
-    g_nat_beq = new name{"Nat", "beq"};
-    g_nat_ble = new name{"Nat", "ble"};
     g_ne = new name{"ne"};
     g_neq_of_not_iff = new name{"neqOfNotIff"};
     g_not = new name{"Not"};
@@ -491,10 +311,7 @@ void initialize_constants() {
     g_opt_param = new name{"optParam"};
     g_or = new name{"Or"};
     g_out_param = new name{"outParam"};
-    g_pexpr = new name{"pexpr"};
-    g_pexpr_subst = new name{"pexpr", "subst"};
     g_punit = new name{"PUnit"};
-    g_punit_cases_on = new name{"PUnit", "casesOn"};
     g_punit_unit = new name{"PUnit", "unit"};
     g_prod_mk = new name{"Prod", "mk"};
     g_pprod = new name{"PProd"};
@@ -502,67 +319,42 @@ void initialize_constants() {
     g_pprod_fst = new name{"PProd", "fst"};
     g_pprod_snd = new name{"PProd", "snd"};
     g_propext = new name{"propext"};
-    g_to_pexpr = new name{"toPexpr"};
     g_quot_mk = new name{"Quot", "mk"};
     g_quot_lift = new name{"Quot", "lift"};
-    g_reflected = new name{"reflected"};
-    g_reflected_subst = new name{"reflected", "subst"};
     g_repr = new name{"repr"};
     g_rfl = new name{"rfl"};
     g_scope_trace = new name{"scopeTrace"};
     g_set_of = new name{"setOf"};
     g_psigma = new name{"PSigma"};
-    g_psigma_cases_on = new name{"PSigma", "casesOn"};
     g_psigma_mk = new name{"PSigma", "mk"};
     g_psigma_fst = new name{"PSigma", "fst"};
     g_psigma_snd = new name{"PSigma", "snd"};
     g_singleton = new name{"singleton"};
-    g_sizeof = new name{"sizeof"};
     g_sorry_ax = new name{"sorryAx"};
     g_string = new name{"String"};
-    g_string_decidable_eq = new name{"String", "DecidableEq"};
-    g_string_mk = new name{"String", "mk"};
     g_string_data = new name{"String", "data"};
     g_string_empty = new name{"String", "Empty"};
     g_string_str = new name{"String", "str"};
-    g_string_empty_ne_str = new name{"String", "emptyNeStr"};
-    g_string_str_ne_empty = new name{"String", "strNeEmpty"};
-    g_string_str_ne_str_left = new name{"String", "strNeStrLeft"};
-    g_string_str_ne_str_right = new name{"String", "strNeStrRight"};
     g_subsingleton = new name{"subsingleton"};
     g_subsingleton_elim = new name{"subsingleton", "elim"};
     g_subtype = new name{"Subtype"};
-    g_subtype_mk = new name{"Subtype", "mk"};
-    g_subtype_val = new name{"Subtype", "val"};
-    g_subtype_rec = new name{"Subtype", "rec"};
     g_psum = new name{"PSum"};
     g_psum_cases_on = new name{"PSum", "casesOn"};
     g_psum_inl = new name{"PSum", "inl"};
     g_psum_inr = new name{"PSum", "inr"};
-    g_tactic = new name{"tactic"};
-    g_tactic_try = new name{"tactic", "try"};
-    g_tactic_triv = new name{"tactic", "triv"};
-    g_tactic_mk_inj_eq = new name{"tactic", "mkInjEq"};
     g_task = new name{"Task"};
     g_thunk = new name{"Thunk"};
-    g_thunk_mk = new name{"Thunk", "mk"};
-    g_trans_rel_left = new name{"transRelLeft"};
-    g_trans_rel_right = new name{"transRelRight"};
     g_true = new name{"True"};
     g_true_intro = new name{"True", "intro"};
     g_typed_expr = new name{"typedExpr"};
     g_unit = new name{"Unit"};
     g_unit_unit = new name{"Unit", "unit"};
-    g_monad_from_pure_bind = new name{"monadFromPureBind"};
     g_uint8 = new name{"UInt8"};
     g_uint16 = new name{"UInt16"};
     g_uint32 = new name{"UInt32"};
     g_uint64 = new name{"UInt64"};
     g_usize = new name{"USize"};
-    g_user_attribute = new name{"userAttribute"};
-    g_user_attribute_parse_reflect = new name{"userAttribute", "parseReflect"};
     g_well_founded_fix = new name{"WellFounded", "fix"};
-    g_well_founded_fix_eq = new name{"WellFounded", "fixEq"};
     g_well_founded_tactics = new name{"wellFoundedTactics"};
     g_well_founded_tactics_default = new name{"wellFoundedTactics", "default"};
     g_well_founded_tactics_rel_tac = new name{"wellFoundedTactics", "relTac"};
@@ -571,8 +363,6 @@ void initialize_constants() {
 }
 void finalize_constants() {
     delete g_absurd;
-    delete g_acc_cases_on;
-    delete g_acc_rec;
     delete g_and;
     delete g_and_left;
     delete g_and_right;
@@ -583,21 +373,13 @@ void finalize_constants() {
     delete g_auto_param;
     delete g_bit0;
     delete g_bit1;
-    delete g_bin_tree_empty;
-    delete g_bin_tree_leaf;
-    delete g_bin_tree_node;
     delete g_bool;
     delete g_bool_false;
     delete g_bool_true;
-    delete g_combinator_k;
     delete g_cast;
     delete g_char;
     delete g_char_mk;
-    delete g_char_ne_of_vne;
     delete g_char_of_nat;
-    delete g_char_of_nat_ne_of_ne;
-    delete g_is_valid_char_range1;
-    delete g_is_valid_char_range2;
     delete g_coe;
     delete g_coe_fn;
     delete g_coe_sort;
@@ -608,8 +390,6 @@ void finalize_constants() {
     delete g_decidable;
     delete g_decidable_cases_on;
     delete g_decidable_to_bool;
-    delete g_decidable_is_true;
-    delete g_decidable_is_false;
     delete g_dite;
     delete g_empty;
     delete g_exists;
@@ -630,22 +410,15 @@ void finalize_constants() {
     delete g_eq_self_iff_true;
     delete g_lean_level;
     delete g_lean_expr;
-    delete g_lean_expr_subst;
     delete g_false;
     delete g_false_of_true_iff_false;
     delete g_false_of_true_eq_false;
     delete g_false_rec;
     delete g_false_cases_on;
     delete g_fin_mk;
-    delete g_fin_ne_of_vne;
-    delete g_forall_congr;
-    delete g_forall_congr_eq;
     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_div;
     delete g_has_emptyc_emptyc;
     delete g_has_eval;
@@ -654,10 +427,7 @@ void finalize_constants() {
     delete g_has_neg_neg;
     delete g_has_one;
     delete g_has_one_one;
-    delete g_has_orelse_orelse;
     delete g_has_sep_sep;
-    delete g_has_sizeof;
-    delete g_has_sizeof_mk;
     delete g_has_sub_sub;
     delete g_has_repr;
     delete g_has_well_founded;
@@ -674,38 +444,19 @@ void finalize_constants() {
     delete g_id;
     delete g_id_rhs;
     delete g_id_delta;
-    delete g_if_neg;
-    delete g_if_pos;
-    delete g_iff;
     delete g_iff_false_intro;
-    delete g_iff_intro;
+    delete g_iff;
     delete g_iff_mp;
     delete g_iff_mpr;
     delete g_iff_refl;
     delete g_iff_symm;
     delete g_iff_trans;
     delete g_iff_true_intro;
-    delete g_imp_congr;
-    delete g_imp_congr_eq;
-    delete g_imp_congr_ctx;
-    delete g_imp_congr_ctx_eq;
-    delete g_implies;
-    delete g_implies_of_if_neg;
-    delete g_implies_of_if_pos;
     delete g_int;
     delete g_int_nat_abs;
     delete g_int_lt;
     delete g_int_dec_lt;
     delete g_int_of_nat;
-    delete g_int_neg_succ_of_nat;
-    delete g_interactive_param_desc;
-    delete g_interactive_parse;
-    delete g_monad_io_impl;
-    delete g_monad_io_terminal_impl;
-    delete g_monad_io_file_system_impl;
-    delete g_monad_io_environment_impl;
-    delete g_monad_io_process_impl;
-    delete g_monad_io_random_impl;
     delete g_inline;
     delete g_io;
     delete g_ite;
@@ -721,11 +472,6 @@ void finalize_constants() {
     delete g_lean_name_anonymous;
     delete g_lean_name_mk_numeral;
     delete g_lean_name_mk_string;
-    delete g_lean_name_no_confusion;
-    delete g_lean_name_mk_string_ne_mk_string_of_ne_prefix;
-    delete g_lean_name_mk_string_ne_mk_string_of_ne_string;
-    delete g_lean_name_mk_numeral_ne_mk_numeral_of_ne_prefix;
-    delete g_lean_name_mk_numeral_ne_mk_numeral_of_ne_numeral;
     delete g_nat;
     delete g_nat_succ;
     delete g_nat_zero;
@@ -733,38 +479,8 @@ void finalize_constants() {
     delete g_nat_has_one;
     delete g_nat_has_add;
     delete g_nat_add;
-    delete g_nat_cases_on;
-    delete g_nat_bit0_ne;
-    delete g_nat_bit0_ne_bit1;
-    delete g_nat_bit0_ne_zero;
-    delete g_nat_bit0_ne_one;
-    delete g_nat_bit1_ne;
-    delete g_nat_bit1_ne_bit0;
-    delete g_nat_bit1_ne_zero;
-    delete g_nat_bit1_ne_one;
-    delete g_nat_zero_ne_one;
-    delete g_nat_zero_ne_bit0;
-    delete g_nat_zero_ne_bit1;
-    delete g_nat_one_ne_zero;
-    delete g_nat_one_ne_bit0;
-    delete g_nat_one_ne_bit1;
-    delete g_nat_bit0_lt;
-    delete g_nat_bit1_lt;
-    delete g_nat_bit0_lt_bit1;
-    delete g_nat_bit1_lt_bit0;
-    delete g_nat_zero_lt_one;
-    delete g_nat_zero_lt_bit1;
-    delete g_nat_zero_lt_bit0;
-    delete g_nat_one_lt_bit0;
-    delete g_nat_one_lt_bit1;
-    delete g_nat_le_of_lt;
-    delete g_nat_le_refl;
-    delete g_nat_decidable_lt;
     delete g_nat_dec_eq;
-    delete g_nat_mul;
     delete g_nat_sub;
-    delete g_nat_beq;
-    delete g_nat_ble;
     delete g_ne;
     delete g_neq_of_not_iff;
     delete g_not;
@@ -775,10 +491,7 @@ void finalize_constants() {
     delete g_opt_param;
     delete g_or;
     delete g_out_param;
-    delete g_pexpr;
-    delete g_pexpr_subst;
     delete g_punit;
-    delete g_punit_cases_on;
     delete g_punit_unit;
     delete g_prod_mk;
     delete g_pprod;
@@ -786,67 +499,42 @@ void finalize_constants() {
     delete g_pprod_fst;
     delete g_pprod_snd;
     delete g_propext;
-    delete g_to_pexpr;
     delete g_quot_mk;
     delete g_quot_lift;
-    delete g_reflected;
-    delete g_reflected_subst;
     delete g_repr;
     delete g_rfl;
     delete g_scope_trace;
     delete g_set_of;
     delete g_psigma;
-    delete g_psigma_cases_on;
     delete g_psigma_mk;
     delete g_psigma_fst;
     delete g_psigma_snd;
     delete g_singleton;
-    delete g_sizeof;
     delete g_sorry_ax;
     delete g_string;
-    delete g_string_decidable_eq;
-    delete g_string_mk;
     delete g_string_data;
     delete g_string_empty;
     delete g_string_str;
-    delete g_string_empty_ne_str;
-    delete g_string_str_ne_empty;
-    delete g_string_str_ne_str_left;
-    delete g_string_str_ne_str_right;
     delete g_subsingleton;
     delete g_subsingleton_elim;
     delete g_subtype;
-    delete g_subtype_mk;
-    delete g_subtype_val;
-    delete g_subtype_rec;
     delete g_psum;
     delete g_psum_cases_on;
     delete g_psum_inl;
     delete g_psum_inr;
-    delete g_tactic;
-    delete g_tactic_try;
-    delete g_tactic_triv;
-    delete g_tactic_mk_inj_eq;
     delete g_task;
     delete g_thunk;
-    delete g_thunk_mk;
-    delete g_trans_rel_left;
-    delete g_trans_rel_right;
     delete g_true;
     delete g_true_intro;
     delete g_typed_expr;
     delete g_unit;
     delete g_unit_unit;
-    delete g_monad_from_pure_bind;
     delete g_uint8;
     delete g_uint16;
     delete g_uint32;
     delete g_uint64;
     delete g_usize;
-    delete g_user_attribute;
-    delete g_user_attribute_parse_reflect;
     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;
@@ -854,8 +542,6 @@ void finalize_constants() {
     delete g_wf_term_hack;
 }
 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_and_name() { return *g_and; }
 name const & get_and_left_name() { return *g_and_left; }
 name const & get_and_right_name() { return *g_and_right; }
@@ -866,21 +552,13 @@ name const & get_array_name() { return *g_array; }
 name const & get_auto_param_name() { return *g_auto_param; }
 name const & get_bit0_name() { return *g_bit0; }
 name const & get_bit1_name() { return *g_bit1; }
-name const & get_bin_tree_empty_name() { return *g_bin_tree_empty; }
-name const & get_bin_tree_leaf_name() { return *g_bin_tree_leaf; }
-name const & get_bin_tree_node_name() { return *g_bin_tree_node; }
 name const & get_bool_name() { return *g_bool; }
 name const & get_bool_false_name() { return *g_bool_false; }
 name const & get_bool_true_name() { return *g_bool_true; }
-name const & get_combinator_k_name() { return *g_combinator_k; }
 name const & get_cast_name() { return *g_cast; }
 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; }
 name const & get_char_of_nat_name() { return *g_char_of_nat; }
-name const & get_char_of_nat_ne_of_ne_name() { return *g_char_of_nat_ne_of_ne; }
-name const & get_is_valid_char_range1_name() { return *g_is_valid_char_range1; }
-name const & get_is_valid_char_range2_name() { return *g_is_valid_char_range2; }
 name const & get_coe_name() { return *g_coe; }
 name const & get_coe_fn_name() { return *g_coe_fn; }
 name const & get_coe_sort_name() { return *g_coe_sort; }
@@ -891,8 +569,6 @@ name const & get_congr_fun_name() { return *g_congr_fun; }
 name const & get_decidable_name() { return *g_decidable; }
 name const & get_decidable_cases_on_name() { return *g_decidable_cases_on; }
 name const & get_decidable_to_bool_name() { return *g_decidable_to_bool; }
-name const & get_decidable_is_true_name() { return *g_decidable_is_true; }
-name const & get_decidable_is_false_name() { return *g_decidable_is_false; }
 name const & get_dite_name() { return *g_dite; }
 name const & get_empty_name() { return *g_empty; }
 name const & get_exists_name() { return *g_exists; }
@@ -913,22 +589,15 @@ 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_lean_level_name() { return *g_lean_level; }
 name const & get_lean_expr_name() { return *g_lean_expr; }
-name const & get_lean_expr_subst_name() { return *g_lean_expr_subst; }
 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_false_rec_name() { return *g_false_rec; }
 name const & get_false_cases_on_name() { return *g_false_cases_on; }
 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_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_div_name() { return *g_has_div_div; }
 name const & get_has_emptyc_emptyc_name() { return *g_has_emptyc_emptyc; }
 name const & get_has_eval_name() { return *g_has_eval; }
@@ -937,10 +606,7 @@ name const & get_has_insert_insert_name() { return *g_has_insert_insert; }
 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; }
-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_sub_name() { return *g_has_sub_sub; }
 name const & get_has_repr_name() { return *g_has_repr; }
 name const & get_has_well_founded_name() { return *g_has_well_founded; }
@@ -957,38 +623,19 @@ name const & get_heq_of_eq_name() { return *g_heq_of_eq; }
 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; }
-name const & get_if_neg_name() { return *g_if_neg; }
-name const & get_if_pos_name() { return *g_if_pos; }
-name const & get_iff_name() { return *g_iff; }
 name const & get_iff_false_intro_name() { return *g_iff_false_intro; }
-name const & get_iff_intro_name() { return *g_iff_intro; }
+name const & get_iff_name() { return *g_iff; }
 name const & get_iff_mp_name() { return *g_iff_mp; }
 name const & get_iff_mpr_name() { return *g_iff_mpr; }
 name const & get_iff_refl_name() { return *g_iff_refl; }
 name const & get_iff_symm_name() { return *g_iff_symm; }
 name const & get_iff_trans_name() { return *g_iff_trans; }
 name const & get_iff_true_intro_name() { return *g_iff_true_intro; }
-name const & get_imp_congr_name() { return *g_imp_congr; }
-name const & get_imp_congr_eq_name() { return *g_imp_congr_eq; }
-name const & get_imp_congr_ctx_name() { return *g_imp_congr_ctx; }
-name const & get_imp_congr_ctx_eq_name() { return *g_imp_congr_ctx_eq; }
-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_nat_abs_name() { return *g_int_nat_abs; }
 name const & get_int_lt_name() { return *g_int_lt; }
 name const & get_int_dec_lt_name() { return *g_int_dec_lt; }
 name const & get_int_of_nat_name() { return *g_int_of_nat; }
-name const & get_int_neg_succ_of_nat_name() { return *g_int_neg_succ_of_nat; }
-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_monad_io_impl_name() { return *g_monad_io_impl; }
-name const & get_monad_io_terminal_impl_name() { return *g_monad_io_terminal_impl; }
-name const & get_monad_io_file_system_impl_name() { return *g_monad_io_file_system_impl; }
-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_inline_name() { return *g_inline; }
 name const & get_io_name() { return *g_io; }
 name const & get_ite_name() { return *g_ite; }
@@ -1004,11 +651,6 @@ name const & get_lean_name_name() { return *g_lean_name; }
 name const & get_lean_name_anonymous_name() { return *g_lean_name_anonymous; }
 name const & get_lean_name_mk_numeral_name() { return *g_lean_name_mk_numeral; }
 name const & get_lean_name_mk_string_name() { return *g_lean_name_mk_string; }
-name const & get_lean_name_no_confusion_name() { return *g_lean_name_no_confusion; }
-name const & get_lean_name_mk_string_ne_mk_string_of_ne_prefix_name() { return *g_lean_name_mk_string_ne_mk_string_of_ne_prefix; }
-name const & get_lean_name_mk_string_ne_mk_string_of_ne_string_name() { return *g_lean_name_mk_string_ne_mk_string_of_ne_string; }
-name const & get_lean_name_mk_numeral_ne_mk_numeral_of_ne_prefix_name() { return *g_lean_name_mk_numeral_ne_mk_numeral_of_ne_prefix; }
-name const & get_lean_name_mk_numeral_ne_mk_numeral_of_ne_numeral_name() { return *g_lean_name_mk_numeral_ne_mk_numeral_of_ne_numeral; }
 name const & get_nat_name() { return *g_nat; }
 name const & get_nat_succ_name() { return *g_nat_succ; }
 name const & get_nat_zero_name() { return *g_nat_zero; }
@@ -1016,38 +658,8 @@ name const & get_nat_has_zero_name() { return *g_nat_has_zero; }
 name const & get_nat_has_one_name() { return *g_nat_has_one; }
 name const & get_nat_has_add_name() { return *g_nat_has_add; }
 name const & get_nat_add_name() { return *g_nat_add; }
-name const & get_nat_cases_on_name() { return *g_nat_cases_on; }
-name const & get_nat_bit0_ne_name() { return *g_nat_bit0_ne; }
-name const & get_nat_bit0_ne_bit1_name() { return *g_nat_bit0_ne_bit1; }
-name const & get_nat_bit0_ne_zero_name() { return *g_nat_bit0_ne_zero; }
-name const & get_nat_bit0_ne_one_name() { return *g_nat_bit0_ne_one; }
-name const & get_nat_bit1_ne_name() { return *g_nat_bit1_ne; }
-name const & get_nat_bit1_ne_bit0_name() { return *g_nat_bit1_ne_bit0; }
-name const & get_nat_bit1_ne_zero_name() { return *g_nat_bit1_ne_zero; }
-name const & get_nat_bit1_ne_one_name() { return *g_nat_bit1_ne_one; }
-name const & get_nat_zero_ne_one_name() { return *g_nat_zero_ne_one; }
-name const & get_nat_zero_ne_bit0_name() { return *g_nat_zero_ne_bit0; }
-name const & get_nat_zero_ne_bit1_name() { return *g_nat_zero_ne_bit1; }
-name const & get_nat_one_ne_zero_name() { return *g_nat_one_ne_zero; }
-name const & get_nat_one_ne_bit0_name() { return *g_nat_one_ne_bit0; }
-name const & get_nat_one_ne_bit1_name() { return *g_nat_one_ne_bit1; }
-name const & get_nat_bit0_lt_name() { return *g_nat_bit0_lt; }
-name const & get_nat_bit1_lt_name() { return *g_nat_bit1_lt; }
-name const & get_nat_bit0_lt_bit1_name() { return *g_nat_bit0_lt_bit1; }
-name const & get_nat_bit1_lt_bit0_name() { return *g_nat_bit1_lt_bit0; }
-name const & get_nat_zero_lt_one_name() { return *g_nat_zero_lt_one; }
-name const & get_nat_zero_lt_bit1_name() { return *g_nat_zero_lt_bit1; }
-name const & get_nat_zero_lt_bit0_name() { return *g_nat_zero_lt_bit0; }
-name const & get_nat_one_lt_bit0_name() { return *g_nat_one_lt_bit0; }
-name const & get_nat_one_lt_bit1_name() { return *g_nat_one_lt_bit1; }
-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_nat_decidable_lt_name() { return *g_nat_decidable_lt; }
 name const & get_nat_dec_eq_name() { return *g_nat_dec_eq; }
-name const & get_nat_mul_name() { return *g_nat_mul; }
 name const & get_nat_sub_name() { return *g_nat_sub; }
-name const & get_nat_beq_name() { return *g_nat_beq; }
-name const & get_nat_ble_name() { return *g_nat_ble; }
 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_not_name() { return *g_not; }
@@ -1058,10 +670,7 @@ name const & get_of_iff_true_name() { return *g_of_iff_true; }
 name const & get_opt_param_name() { return *g_opt_param; }
 name const & get_or_name() { return *g_or; }
 name const & get_out_param_name() { return *g_out_param; }
-name const & get_pexpr_name() { return *g_pexpr; }
-name const & get_pexpr_subst_name() { return *g_pexpr_subst; }
 name const & get_punit_name() { return *g_punit; }
-name const & get_punit_cases_on_name() { return *g_punit_cases_on; }
 name const & get_punit_unit_name() { return *g_punit_unit; }
 name const & get_prod_mk_name() { return *g_prod_mk; }
 name const & get_pprod_name() { return *g_pprod; }
@@ -1069,67 +678,42 @@ name const & get_pprod_mk_name() { return *g_pprod_mk; }
 name const & get_pprod_fst_name() { return *g_pprod_fst; }
 name const & get_pprod_snd_name() { return *g_pprod_snd; }
 name const & get_propext_name() { return *g_propext; }
-name const & get_to_pexpr_name() { return *g_to_pexpr; }
 name const & get_quot_mk_name() { return *g_quot_mk; }
 name const & get_quot_lift_name() { return *g_quot_lift; }
-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_scope_trace_name() { return *g_scope_trace; }
 name const & get_set_of_name() { return *g_set_of; }
 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; }
 name const & get_psigma_fst_name() { return *g_psigma_fst; }
 name const & get_psigma_snd_name() { return *g_psigma_snd; }
 name const & get_singleton_name() { return *g_singleton; }
-name const & get_sizeof_name() { return *g_sizeof; }
 name const & get_sorry_ax_name() { return *g_sorry_ax; }
 name const & get_string_name() { return *g_string; }
-name const & get_string_decidable_eq_name() { return *g_string_decidable_eq; }
-name const & get_string_mk_name() { return *g_string_mk; }
 name const & get_string_data_name() { return *g_string_data; }
 name const & get_string_empty_name() { return *g_string_empty; }
 name const & get_string_str_name() { return *g_string_str; }
-name const & get_string_empty_ne_str_name() { return *g_string_empty_ne_str; }
-name const & get_string_str_ne_empty_name() { return *g_string_str_ne_empty; }
-name const & get_string_str_ne_str_left_name() { return *g_string_str_ne_str_left; }
-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_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; }
-name const & get_subtype_rec_name() { return *g_subtype_rec; }
 name const & get_psum_name() { return *g_psum; }
 name const & get_psum_cases_on_name() { return *g_psum_cases_on; }
 name const & get_psum_inl_name() { return *g_psum_inl; }
 name const & get_psum_inr_name() { return *g_psum_inr; }
-name const & get_tactic_name() { return *g_tactic; }
-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_task_name() { return *g_task; }
 name const & get_thunk_name() { return *g_thunk; }
-name const & get_thunk_mk_name() { return *g_thunk_mk; }
-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_unit_name() { return *g_unit; }
 name const & get_unit_unit_name() { return *g_unit_unit; }
-name const & get_monad_from_pure_bind_name() { return *g_monad_from_pure_bind; }
 name const & get_uint8_name() { return *g_uint8; }
 name const & get_uint16_name() { return *g_uint16; }
 name const & get_uint32_name() { return *g_uint32; }
 name const & get_uint64_name() { return *g_uint64; }
 name const & get_usize_name() { return *g_usize; }
-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_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; }

src/library/constants.h

@@ -6,8 +6,6 @@ namespace lean {
 void initialize_constants();
 void finalize_constants();
 name const & get_absurd_name();
-name const & get_acc_cases_on_name();
-name const & get_acc_rec_name();
 name const & get_and_name();
 name const & get_and_left_name();
 name const & get_and_right_name();
@@ -18,21 +16,13 @@ name const & get_array_name();
 name const & get_auto_param_name();
 name const & get_bit0_name();
 name const & get_bit1_name();
-name const & get_bin_tree_empty_name();
-name const & get_bin_tree_leaf_name();
-name const & get_bin_tree_node_name();
 name const & get_bool_name();
 name const & get_bool_false_name();
 name const & get_bool_true_name();
-name const & get_combinator_k_name();
 name const & get_cast_name();
 name const & get_char_name();
 name const & get_char_mk_name();
-name const & get_char_ne_of_vne_name();
 name const & get_char_of_nat_name();
-name const & get_char_of_nat_ne_of_ne_name();
-name const & get_is_valid_char_range1_name();
-name const & get_is_valid_char_range2_name();
 name const & get_coe_name();
 name const & get_coe_fn_name();
 name const & get_coe_sort_name();
@@ -43,8 +33,6 @@ name const & get_congr_fun_name();
 name const & get_decidable_name();
 name const & get_decidable_cases_on_name();
 name const & get_decidable_to_bool_name();
-name const & get_decidable_is_true_name();
-name const & get_decidable_is_false_name();
 name const & get_dite_name();
 name const & get_empty_name();
 name const & get_exists_name();
@@ -65,22 +53,15 @@ name const & get_eq_false_intro_name();
 name const & get_eq_self_iff_true_name();
 name const & get_lean_level_name();
 name const & get_lean_expr_name();
-name const & get_lean_expr_subst_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_false_rec_name();
 name const & get_false_cases_on_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_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_div_name();
 name const & get_has_emptyc_emptyc_name();
 name const & get_has_eval_name();
@@ -89,10 +70,7 @@ name const & get_has_insert_insert_name();
 name const & get_has_neg_neg_name();
 name const & get_has_one_name();
 name const & get_has_one_one_name();
-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_sub_name();
 name const & get_has_repr_name();
 name const & get_has_well_founded_name();
@@ -109,38 +87,19 @@ name const & get_heq_of_eq_name();
 name const & get_id_name();
 name const & get_id_rhs_name();
 name const & get_id_delta_name();
-name const & get_if_neg_name();
-name const & get_if_pos_name();
-name const & get_iff_name();
 name const & get_iff_false_intro_name();
-name const & get_iff_intro_name();
+name const & get_iff_name();
 name const & get_iff_mp_name();
 name const & get_iff_mpr_name();
 name const & get_iff_refl_name();
 name const & get_iff_symm_name();
 name const & get_iff_trans_name();
 name const & get_iff_true_intro_name();
-name const & get_imp_congr_name();
-name const & get_imp_congr_eq_name();
-name const & get_imp_congr_ctx_name();
-name const & get_imp_congr_ctx_eq_name();
-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_nat_abs_name();
 name const & get_int_lt_name();
 name const & get_int_dec_lt_name();
 name const & get_int_of_nat_name();
-name const & get_int_neg_succ_of_nat_name();
-name const & get_interactive_param_desc_name();
-name const & get_interactive_parse_name();
-name const & get_monad_io_impl_name();
-name const & get_monad_io_terminal_impl_name();
-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_inline_name();
 name const & get_io_name();
 name const & get_ite_name();
@@ -156,11 +115,6 @@ name const & get_lean_name_name();
 name const & get_lean_name_anonymous_name();
 name const & get_lean_name_mk_numeral_name();
 name const & get_lean_name_mk_string_name();
-name const & get_lean_name_no_confusion_name();
-name const & get_lean_name_mk_string_ne_mk_string_of_ne_prefix_name();
-name const & get_lean_name_mk_string_ne_mk_string_of_ne_string_name();
-name const & get_lean_name_mk_numeral_ne_mk_numeral_of_ne_prefix_name();
-name const & get_lean_name_mk_numeral_ne_mk_numeral_of_ne_numeral_name();
 name const & get_nat_name();
 name const & get_nat_succ_name();
 name const & get_nat_zero_name();
@@ -168,38 +122,8 @@ name const & get_nat_has_zero_name();
 name const & get_nat_has_one_name();
 name const & get_nat_has_add_name();
 name const & get_nat_add_name();
-name const & get_nat_cases_on_name();
-name const & get_nat_bit0_ne_name();
-name const & get_nat_bit0_ne_bit1_name();
-name const & get_nat_bit0_ne_zero_name();
-name const & get_nat_bit0_ne_one_name();
-name const & get_nat_bit1_ne_name();
-name const & get_nat_bit1_ne_bit0_name();
-name const & get_nat_bit1_ne_zero_name();
-name const & get_nat_bit1_ne_one_name();
-name const & get_nat_zero_ne_one_name();
-name const & get_nat_zero_ne_bit0_name();
-name const & get_nat_zero_ne_bit1_name();
-name const & get_nat_one_ne_zero_name();
-name const & get_nat_one_ne_bit0_name();
-name const & get_nat_one_ne_bit1_name();
-name const & get_nat_bit0_lt_name();
-name const & get_nat_bit1_lt_name();
-name const & get_nat_bit0_lt_bit1_name();
-name const & get_nat_bit1_lt_bit0_name();
-name const & get_nat_zero_lt_one_name();
-name const & get_nat_zero_lt_bit1_name();
-name const & get_nat_zero_lt_bit0_name();
-name const & get_nat_one_lt_bit0_name();
-name const & get_nat_one_lt_bit1_name();
-name const & get_nat_le_of_lt_name();
-name const & get_nat_le_refl_name();
-name const & get_nat_decidable_lt_name();
 name const & get_nat_dec_eq_name();
-name const & get_nat_mul_name();
 name const & get_nat_sub_name();
-name const & get_nat_beq_name();
-name const & get_nat_ble_name();
 name const & get_ne_name();
 name const & get_neq_of_not_iff_name();
 name const & get_not_name();
@@ -210,10 +134,7 @@ name const & get_of_iff_true_name();
 name const & get_opt_param_name();
 name const & get_or_name();
 name const & get_out_param_name();
-name const & get_pexpr_name();
-name const & get_pexpr_subst_name();
 name const & get_punit_name();
-name const & get_punit_cases_on_name();
 name const & get_punit_unit_name();
 name const & get_prod_mk_name();
 name const & get_pprod_name();
@@ -221,67 +142,42 @@ name const & get_pprod_mk_name();
 name const & get_pprod_fst_name();
 name const & get_pprod_snd_name();
 name const & get_propext_name();
-name const & get_to_pexpr_name();
 name const & get_quot_mk_name();
 name const & get_quot_lift_name();
-name const & get_reflected_name();
-name const & get_reflected_subst_name();
 name const & get_repr_name();
 name const & get_rfl_name();
 name const & get_scope_trace_name();
 name const & get_set_of_name();
 name const & get_psigma_name();
-name const & get_psigma_cases_on_name();
 name const & get_psigma_mk_name();
 name const & get_psigma_fst_name();
 name const & get_psigma_snd_name();
 name const & get_singleton_name();
-name const & get_sizeof_name();
 name const & get_sorry_ax_name();
 name const & get_string_name();
-name const & get_string_decidable_eq_name();
-name const & get_string_mk_name();
 name const & get_string_data_name();
 name const & get_string_empty_name();
 name const & get_string_str_name();
-name const & get_string_empty_ne_str_name();
-name const & get_string_str_ne_empty_name();
-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_subtype_name();
-name const & get_subtype_mk_name();
-name const & get_subtype_val_name();
-name const & get_subtype_rec_name();
 name const & get_psum_name();
 name const & get_psum_cases_on_name();
 name const & get_psum_inl_name();
 name const & get_psum_inr_name();
-name const & get_tactic_name();
-name const & get_tactic_try_name();
-name const & get_tactic_triv_name();
-name const & get_tactic_mk_inj_eq_name();
 name const & get_task_name();
 name const & get_thunk_name();
-name const & get_thunk_mk_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_unit_name();
 name const & get_unit_unit_name();
-name const & get_monad_from_pure_bind_name();
 name const & get_uint8_name();
 name const & get_uint16_name();
 name const & get_uint32_name();
 name const & get_uint64_name();
 name const & get_usize_name();
-name const & get_user_attribute_name();
-name const & get_user_attribute_parse_reflect_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();

src/library/constants.txt

@@ -1,6 +1,4 @@
 absurd
-Acc.casesOn
-Acc.rec
 And
 And.left
 And.right
@@ -11,21 +9,13 @@ Array
 autoParam
 bit0
 bit1
-BinTree.Empty
-BinTree.leaf
-BinTree.Node
 Bool
 Bool.false
 Bool.true
-Combinator.K
 cast
 Char
 Char.mk
-Char.neOfVne
 Char.ofNat
-Char.ofNatNeOfNe
-isValidCharRange1
-isValidCharRange2
 coe
 coeFn
 coeSort
@@ -36,8 +26,6 @@ congrFun
 Decidable
 Decidable.casesOn
 Decidable.toBool
-Decidable.isTrue
-Decidable.isFalse
 dite
 Empty
 Exists
@@ -58,22 +46,15 @@ eqFalseIntro
 eqSelfIffTrue
 Lean.Level
 Lean.Expr
-Lean.Expr.subst
 False
 falseOfTrueIffFalse
 falseOfTrueEqFalse
 False.rec
 False.casesOn
 Fin.mk
-Fin.neOfVne
-forallCongr
-forallCongrEq
 funext
 HasAdd
 HasAdd.add
-HasAndthen.andthen
-HasBind.andThen
-HasBind.Seq
 HasDiv.div
 HasEmptyc.emptyc
 HasEval
@@ -82,10 +63,7 @@ HasInsert.insert
 HasNeg.neg
 HasOne
 HasOne.one
-HasOrelse.orelse
 HasSep.sep
-HasSizeof
-HasSizeof.mk
 HasSub.sub
 HasRepr
 HasWellFounded
@@ -102,38 +80,19 @@ heqOfEq
 id
 idRhs
 idDelta
-ifNeg
-ifPos
-Iff
 iffFalseIntro
-Iff.intro
+Iff
 Iff.mp
 Iff.mpr
 Iff.refl
 Iff.symm
 Iff.trans
 iffTrueIntro
-impCongr
-impCongrEq
-impCongrCtx
-impCongrCtxEq
-implies
-impliesOfIfNeg
-impliesOfIfPos
 Int
 Int.natAbs
 Int.lt
 Int.decLt
 Int.ofNat
-Int.negSuccOfNat
-interactive.paramDesc
-interactive.parse
-monadIOImpl
-monadIOTerminalImpl
-monadIOFileSystemImpl
-monadIOEnvironmentImpl
-monadIOProcessImpl
-monadIORandomImpl
 inline
 IO
 ite
@@ -149,11 +108,6 @@ Lean.Name
 Lean.Name.anonymous
 Lean.Name.mkNumeral
 Lean.Name.mkString
-Lean.Name.noConfusion
-Lean.Name.mkStringNeMkStringOfNePrefix
-Lean.Name.mkStringNeMkStringOfNeString
-Lean.Name.mkNumeralNeMkNumeralOfNePrefix
-Lean.Name.mkNumeralNeMkNumeralOfNeNumeral
 Nat
 Nat.succ
 Nat.zero
@@ -161,38 +115,8 @@ Nat.HasZero
 Nat.HasOne
 Nat.HasAdd
 Nat.add
-Nat.casesOn
-Nat.bit0Ne
-Nat.bit0NeBit1
-Nat.bit0NeZero
-Nat.bit0NeOne
-Nat.bit1Ne
-Nat.bit1NeBit0
-Nat.bit1NeZero
-Nat.bit1NeOne
-Nat.zeroNeOne
-Nat.zeroNeBit0
-Nat.zeroNeBit1
-Nat.oneNeZero
-Nat.oneNeBit0
-Nat.oneNeBit1
-Nat.bit0Lt
-Nat.bit1Lt
-Nat.bit0LtBit1
-Nat.bit1LtBit0
-Nat.zeroLtOne
-Nat.zeroLtBit1
-Nat.zeroLtBit0
-Nat.oneLtBit0
-Nat.oneLtBit1
-Nat.leOfLt
-Nat.leRefl
-Nat.decidableLt
 Nat.decEq
-Nat.mul
 Nat.sub
-Nat.beq
-Nat.ble
 ne
 neqOfNotIff
 Not
@@ -203,10 +127,7 @@ ofIffTrue
 optParam
 Or
 outParam
-pexpr
-pexpr.subst
 PUnit
-PUnit.casesOn
 PUnit.unit
 Prod.mk
 PProd
@@ -214,67 +135,42 @@ PProd.mk
 PProd.fst
 PProd.snd
 propext
-toPexpr
 Quot.mk
 Quot.lift
-reflected
-reflected.subst
 repr
 rfl
 scopeTrace
 setOf
 PSigma
-PSigma.casesOn
 PSigma.mk
 PSigma.fst
 PSigma.snd
 singleton
-sizeof
 sorryAx
 String
-String.DecidableEq
-String.mk
 String.data
 String.Empty
 String.str
-String.emptyNeStr
-String.strNeEmpty
-String.strNeStrLeft
-String.strNeStrRight
 subsingleton
 subsingleton.elim
 Subtype
-Subtype.mk
-Subtype.val
-Subtype.rec
 PSum
 PSum.casesOn
 PSum.inl
 PSum.inr
-tactic
-tactic.try
-tactic.triv
-tactic.mkInjEq
 Task
 Thunk
-Thunk.mk
-transRelLeft
-transRelRight
 True
 True.intro
 typedExpr
 Unit
 Unit.unit
-monadFromPureBind
 UInt8 uint8
 UInt16 uint16
 UInt32 uint32
 UInt64 uint64
 USize usize
-userAttribute
-userAttribute.parseReflect
 WellFounded.fix
-WellFounded.fixEq
 wellFoundedTactics
 wellFoundedTactics.default
 wellFoundedTactics.relTac

src/library/util.cpp

@@ -1022,12 +1022,6 @@ optional<name> name_lit_to_name(expr const & name_lit) {
     return optional<name>();
 }
 
-static expr * g_tactic_unit = nullptr;
-
-expr mk_tactic_unit() {
-    return *g_tactic_unit;
-}
-
 static std::string * g_version_string = nullptr;
 std::string const & get_version_string() { return *g_version_string; }
 
@@ -1055,7 +1049,6 @@ void initialize_library_util() {
     g_and_intro      = new expr(mk_constant(get_and_intro_name()));
     g_and_left  = new expr(mk_constant(get_and_left_name()));
     g_and_right = new expr(mk_constant(get_and_right_name()));
-    g_tactic_unit    = new expr(mk_app(mk_constant(get_tactic_name(), {mk_level_zero()}), mk_constant(get_unit_name())));
     initialize_nat();
     initialize_int();
     initialize_char();
@@ -1094,7 +1087,6 @@ void finalize_library_util() {
     delete g_and_intro;
     delete g_and_left;
     delete g_and_right;
-    delete g_tactic_unit;
     delete g_unit_mk;
     delete g_unit;
 }

src/library/util.h

@@ -310,9 +310,6 @@ optional<name> is_unsafe_rec_name(name const & n);
 /** Convert an expression representing a `name` literal into a `name` object. */
 optional<name> name_lit_to_name(expr const & name_lit);
 
-/** Return (tactic unit) type */
-expr mk_tactic_unit();
-
 std::string const & get_version_string();
 
 expr const & extract_mdata(expr const &);