sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00
Code Issues Packages Projects Releases Wiki Activity

chore(library): cleanup constants.txt

Browse Source
This commit is contained in:
Leonardo de Moura
2018-04-12 13:29:06 -07:00
parent 8b8c2ddf37
commit 1e11611388
12 changed files with 251 additions and 829 deletions
Download Patch File Download Diff File Expand all files Collapse all files

8
library/init/meta/comp_value_tactics.lean
View File

@@ -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

2
script/gen_constants_cpp.py
View File

@@ -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");

106
src/library/comp_val.cpp
View File

@@ -207,116 +207,10 @@ optional<expr> mk_string_val_ne_proof(expr a, expr b) {
return none_expr();
}
optional<expr> 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<expr> 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<expr_pair> mk_nat_abs_eq(expr const & a) {
if (is_zero(a)) {
return optional<expr_pair>(mk_pair(mk_nat_zero(), mk_constant(get_int_nat_abs_zero_name())));
} else if (is_one(a)) {
return optional<expr_pair>(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<expr_pair>(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<expr_pair>(mk_pair(new_n, new_H));
}
}
return optional<expr_pair>();
}
/* Given nonneg int numerals a and b, create a proof for a != b IF they are not equal. */
optional<expr> 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<expr> 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<expr> 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())))

13
src/library/comp_val.h
View File

@@ -37,19 +37,6 @@ optional<expr> mk_char_val_ne_proof(expr const & a, expr const & b);
/* Similar to mk_nat_val_ne_proof, but for string type */
optional<expr> 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<expr> 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<expr> mk_int_val_pos_proof(expr const & a);
/* Similar to mk_nat_val_ne_proof, but for int type */
optional<expr> 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<expr> mk_val_ne_proof(type_context_old & ctx, expr const & a, expr const & b);

456
src/library/constants.cpp
View File

@@ -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; }
}

114
src/library/constants.h
View File

@@ -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();
}

114
src/library/constants.txt
View File

@@ -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

7
src/library/vm/vm.cpp
View File

@@ -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<vm_monitor_modification>(d));
}
[[noreturn]] void vm_check_failed(char const * condition) {
throw exception(sstream() << "vm check failed: " << condition
<< " (possibly due to incorrect axioms, or sorry)");

2
src/library/vm/vm.h
View File

@@ -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();

5
src/library/vm/vm_expr.cpp
View File

@@ -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);

5
src/library/vm/vm_io.cpp
View File

@@ -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");
}
}

248
tests/lean/run/check_constants.lean Normal file
View File

@@ -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