chore: remove unused names
This commit is contained in:
Leonardo de Moura
parent
ff493751b5
commit
1fba699b2c
3 changed files with 2 additions and 735 deletions
|
|
@ -24,20 +24,11 @@ name const * g_bool_true = nullptr;
|
|||
name const * g_bool_cases_on = nullptr;
|
||||
name const * g_cast = nullptr;
|
||||
name const * g_char = nullptr;
|
||||
name const * g_char_mk = nullptr;
|
||||
name const * g_char_of_nat = nullptr;
|
||||
name const * g_old_coe = nullptr;
|
||||
name const * g_old_coe_fn = nullptr;
|
||||
name const * g_old_coe_sort = nullptr;
|
||||
name const * g_old_coe_to_lift = nullptr;
|
||||
name const * g_congr = nullptr;
|
||||
name const * g_congr_arg = nullptr;
|
||||
name const * g_congr_fun = nullptr;
|
||||
name const * g_decidable = nullptr;
|
||||
name const * g_decidable_is_true = nullptr;
|
||||
name const * g_decidable_is_false = nullptr;
|
||||
name const * g_decidable_decide = nullptr;
|
||||
name const * g_dite = nullptr;
|
||||
name const * g_empty = nullptr;
|
||||
name const * g_empty_rec = nullptr;
|
||||
name const * g_empty_cases_on = nullptr;
|
||||
|
|
@ -46,86 +37,34 @@ name const * g_eq = nullptr;
|
|||
name const * g_eq_cases_on = nullptr;
|
||||
name const * g_eq_rec_on = nullptr;
|
||||
name const * g_eq_rec = nullptr;
|
||||
name const * g_eq_mp = nullptr;
|
||||
name const * g_eq_mpr = nullptr;
|
||||
name const * g_eq_ndrec = nullptr;
|
||||
name const * g_eq_refl = nullptr;
|
||||
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_true_intro = nullptr;
|
||||
name const * g_eq_false_intro = nullptr;
|
||||
name const * g_eq_self_iff_true = nullptr;
|
||||
name const * g_float = nullptr;
|
||||
name const * g_float_array = nullptr;
|
||||
name const * g_lean_message_data = nullptr;
|
||||
name const * g_lean_monad_tracer_trace = 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_funext = nullptr;
|
||||
name const * g_has_add = nullptr;
|
||||
name const * g_has_add_add = nullptr;
|
||||
name const * g_has_div_div = nullptr;
|
||||
name const * g_has_emptyc_emptyc = nullptr;
|
||||
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_sep_sep = nullptr;
|
||||
name const * g_has_sub_sub = nullptr;
|
||||
name const * g_has_well_founded = nullptr;
|
||||
name const * g_has_well_founded_r = nullptr;
|
||||
name const * g_has_well_founded_wf = nullptr;
|
||||
name const * g_has_zero = nullptr;
|
||||
name const * g_has_zero_zero = nullptr;
|
||||
name const * g_has_coe_t = nullptr;
|
||||
name const * g_heq = nullptr;
|
||||
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_huge_fuel = nullptr;
|
||||
name const * g_id = nullptr;
|
||||
name const * g_id_rhs = nullptr;
|
||||
name const * g_id_delta = nullptr;
|
||||
name const * g_iff_false_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_inhabited = nullptr;
|
||||
name const * g_inhabited_default = nullptr;
|
||||
name const * g_int = nullptr;
|
||||
name const * g_int_nat_abs = nullptr;
|
||||
name const * g_int_dec_lt = nullptr;
|
||||
name const * g_int_of_nat = nullptr;
|
||||
name const * g_inline = nullptr;
|
||||
name const * g_eio = nullptr;
|
||||
name const * g_st = nullptr;
|
||||
name const * g_io = nullptr;
|
||||
name const * g_ite = nullptr;
|
||||
name const * g_lc_proof = nullptr;
|
||||
name const * g_lc_unreachable = nullptr;
|
||||
name const * g_list = nullptr;
|
||||
name const * g_list_nil = nullptr;
|
||||
name const * g_list_cons = nullptr;
|
||||
name const * g_list_to_array = nullptr;
|
||||
name const * g_monad = nullptr;
|
||||
name const * g_lean_name_anonymous = nullptr;
|
||||
name const * g_lean_name_num = nullptr;
|
||||
name const * g_lean_name_str = nullptr;
|
||||
name const * g_lean_mk_name_num = nullptr;
|
||||
name const * g_lean_mk_name_str = nullptr;
|
||||
name const * g_lean_parser_leading_node = nullptr;
|
||||
name const * g_lean_parser_trailing_node = nullptr;
|
||||
name const * g_mut_quot = nullptr;
|
||||
name const * g_nat = nullptr;
|
||||
name const * g_nat_succ = nullptr;
|
||||
|
|
@ -137,19 +76,12 @@ name const * g_nat_add = nullptr;
|
|||
name const * g_nat_dec_eq = nullptr;
|
||||
name const * g_nat_sub = nullptr;
|
||||
name const * g_ne = nullptr;
|
||||
name const * g_neq_of_not_iff = nullptr;
|
||||
name const * g_not = nullptr;
|
||||
name const * g_not_of_iff_false = nullptr;
|
||||
name const * g_not_of_eq_false = nullptr;
|
||||
name const * g_of_eq_true = nullptr;
|
||||
name const * g_of_iff_true = nullptr;
|
||||
name const * g_opt_param = nullptr;
|
||||
name const * g_or = nullptr;
|
||||
name const * g_panic = nullptr;
|
||||
name const * g_panic_with_pos = nullptr;
|
||||
name const * g_punit = nullptr;
|
||||
name const * g_punit_unit = nullptr;
|
||||
name const * g_prod_mk = nullptr;
|
||||
name const * g_pprod = nullptr;
|
||||
name const * g_pprod_mk = nullptr;
|
||||
name const * g_pprod_fst = nullptr;
|
||||
|
|
@ -157,33 +89,16 @@ name const * g_pprod_snd = nullptr;
|
|||
name const * g_propext = nullptr;
|
||||
name const * g_quot_mk = nullptr;
|
||||
name const * g_quot_lift = 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_mk = nullptr;
|
||||
name const * g_psigma_fst = nullptr;
|
||||
name const * g_psigma_snd = nullptr;
|
||||
name const * g_singleton = nullptr;
|
||||
name const * g_sorry_ax = nullptr;
|
||||
name const * g_string = nullptr;
|
||||
name const * g_string_data = nullptr;
|
||||
name const * g_string_empty = nullptr;
|
||||
name const * g_string_str = nullptr;
|
||||
name const * g_subsingleton = nullptr;
|
||||
name const * g_subsingleton_elim = nullptr;
|
||||
name const * g_subtype = 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_task = nullptr;
|
||||
name const * g_thunk = nullptr;
|
||||
name const * g_thunk_mk = nullptr;
|
||||
name const * g_thunk_get = 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_uint8 = nullptr;
|
||||
|
|
@ -191,398 +106,110 @@ name const * g_uint16 = nullptr;
|
|||
name const * g_uint32 = nullptr;
|
||||
name const * g_uint64 = nullptr;
|
||||
name const * g_usize = nullptr;
|
||||
name const * g_well_founded_fix = 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;
|
||||
void initialize_constants() {
|
||||
g_absurd = new name{"absurd"};
|
||||
mark_persistent(g_absurd->raw());
|
||||
g_and = new name{"And"};
|
||||
mark_persistent(g_and->raw());
|
||||
g_and_left = new name{"And", "left"};
|
||||
mark_persistent(g_and_left->raw());
|
||||
g_and_right = new name{"And", "right"};
|
||||
mark_persistent(g_and_right->raw());
|
||||
g_and_intro = new name{"And", "intro"};
|
||||
mark_persistent(g_and_intro->raw());
|
||||
g_and_rec = new name{"And", "rec"};
|
||||
mark_persistent(g_and_rec->raw());
|
||||
g_and_cases_on = new name{"And", "casesOn"};
|
||||
mark_persistent(g_and_cases_on->raw());
|
||||
g_array = new name{"Array"};
|
||||
mark_persistent(g_array->raw());
|
||||
g_array_sz = new name{"Array", "sz"};
|
||||
mark_persistent(g_array_sz->raw());
|
||||
g_array_data = new name{"Array", "data"};
|
||||
mark_persistent(g_array_data->raw());
|
||||
g_auto_param = new name{"autoParam"};
|
||||
mark_persistent(g_auto_param->raw());
|
||||
g_bit0 = new name{"bit0"};
|
||||
mark_persistent(g_bit0->raw());
|
||||
g_bit1 = new name{"bit1"};
|
||||
mark_persistent(g_bit1->raw());
|
||||
g_has_of_nat_of_nat = new name{"HasOfNat", "ofNat"};
|
||||
mark_persistent(g_has_of_nat_of_nat->raw());
|
||||
g_byte_array = new name{"ByteArray"};
|
||||
mark_persistent(g_byte_array->raw());
|
||||
g_bool = new name{"Bool"};
|
||||
mark_persistent(g_bool->raw());
|
||||
g_bool_false = new name{"Bool", "false"};
|
||||
mark_persistent(g_bool_false->raw());
|
||||
g_bool_true = new name{"Bool", "true"};
|
||||
mark_persistent(g_bool_true->raw());
|
||||
g_bool_cases_on = new name{"Bool", "casesOn"};
|
||||
mark_persistent(g_bool_cases_on->raw());
|
||||
g_cast = new name{"cast"};
|
||||
mark_persistent(g_cast->raw());
|
||||
g_char = new name{"Char"};
|
||||
mark_persistent(g_char->raw());
|
||||
g_char_mk = new name{"Char", "mk"};
|
||||
mark_persistent(g_char_mk->raw());
|
||||
g_char_of_nat = new name{"Char", "ofNat"};
|
||||
mark_persistent(g_char_of_nat->raw());
|
||||
g_old_coe = new name{"oldCoe"};
|
||||
mark_persistent(g_old_coe->raw());
|
||||
g_old_coe_fn = new name{"oldCoeFn"};
|
||||
mark_persistent(g_old_coe_fn->raw());
|
||||
g_old_coe_sort = new name{"oldCoeSort"};
|
||||
mark_persistent(g_old_coe_sort->raw());
|
||||
g_old_coe_to_lift = new name{"oldCoeToLift"};
|
||||
mark_persistent(g_old_coe_to_lift->raw());
|
||||
g_congr = new name{"congr"};
|
||||
mark_persistent(g_congr->raw());
|
||||
g_congr_arg = new name{"congrArg"};
|
||||
mark_persistent(g_congr_arg->raw());
|
||||
g_congr_fun = new name{"congrFun"};
|
||||
mark_persistent(g_congr_fun->raw());
|
||||
g_decidable = new name{"Decidable"};
|
||||
mark_persistent(g_decidable->raw());
|
||||
g_decidable_is_true = new name{"Decidable", "isTrue"};
|
||||
mark_persistent(g_decidable_is_true->raw());
|
||||
g_decidable_is_false = new name{"Decidable", "isFalse"};
|
||||
mark_persistent(g_decidable_is_false->raw());
|
||||
g_decidable_decide = new name{"Decidable", "decide"};
|
||||
mark_persistent(g_decidable_decide->raw());
|
||||
g_dite = new name{"dite"};
|
||||
mark_persistent(g_dite->raw());
|
||||
g_empty = new name{"Empty"};
|
||||
mark_persistent(g_empty->raw());
|
||||
g_empty_rec = new name{"Empty", "rec"};
|
||||
mark_persistent(g_empty_rec->raw());
|
||||
g_empty_cases_on = new name{"Empty", "casesOn"};
|
||||
mark_persistent(g_empty_cases_on->raw());
|
||||
g_exists = new name{"Exists"};
|
||||
mark_persistent(g_exists->raw());
|
||||
g_eq = new name{"Eq"};
|
||||
mark_persistent(g_eq->raw());
|
||||
g_eq_cases_on = new name{"Eq", "casesOn"};
|
||||
mark_persistent(g_eq_cases_on->raw());
|
||||
g_eq_rec_on = new name{"Eq", "recOn"};
|
||||
mark_persistent(g_eq_rec_on->raw());
|
||||
g_eq_rec = new name{"Eq", "rec"};
|
||||
mark_persistent(g_eq_rec->raw());
|
||||
g_eq_mp = new name{"Eq", "mp"};
|
||||
mark_persistent(g_eq_mp->raw());
|
||||
g_eq_mpr = new name{"Eq", "mpr"};
|
||||
mark_persistent(g_eq_mpr->raw());
|
||||
g_eq_ndrec = new name{"Eq", "ndrec"};
|
||||
mark_persistent(g_eq_ndrec->raw());
|
||||
g_eq_refl = new name{"Eq", "refl"};
|
||||
mark_persistent(g_eq_refl->raw());
|
||||
g_eq_subst = new name{"Eq", "subst"};
|
||||
mark_persistent(g_eq_subst->raw());
|
||||
g_eq_symm = new name{"Eq", "symm"};
|
||||
mark_persistent(g_eq_symm->raw());
|
||||
g_eq_trans = new name{"Eq", "trans"};
|
||||
mark_persistent(g_eq_trans->raw());
|
||||
g_eq_of_heq = new name{"eqOfHEq"};
|
||||
mark_persistent(g_eq_of_heq->raw());
|
||||
g_eq_true_intro = new name{"eqTrueIntro"};
|
||||
mark_persistent(g_eq_true_intro->raw());
|
||||
g_eq_false_intro = new name{"eqFalseIntro"};
|
||||
mark_persistent(g_eq_false_intro->raw());
|
||||
g_eq_self_iff_true = new name{"eqSelfIffTrue"};
|
||||
mark_persistent(g_eq_self_iff_true->raw());
|
||||
g_float = new name{"Float"};
|
||||
mark_persistent(g_float->raw());
|
||||
g_float_array = new name{"FloatArray"};
|
||||
mark_persistent(g_float_array->raw());
|
||||
g_lean_message_data = new name{"Lean", "MessageData"};
|
||||
mark_persistent(g_lean_message_data->raw());
|
||||
g_lean_monad_tracer_trace = new name{"Lean", "MonadTracer", "trace"};
|
||||
mark_persistent(g_lean_monad_tracer_trace->raw());
|
||||
g_false = new name{"False"};
|
||||
mark_persistent(g_false->raw());
|
||||
g_false_of_true_iff_false = new name{"falseOfTrueIffFalse"};
|
||||
mark_persistent(g_false_of_true_iff_false->raw());
|
||||
g_false_of_true_eq_false = new name{"falseOfTrueEqFalse"};
|
||||
mark_persistent(g_false_of_true_eq_false->raw());
|
||||
g_false_rec = new name{"False", "rec"};
|
||||
mark_persistent(g_false_rec->raw());
|
||||
g_false_cases_on = new name{"False", "casesOn"};
|
||||
mark_persistent(g_false_cases_on->raw());
|
||||
g_fin_mk = new name{"Fin", "mk"};
|
||||
mark_persistent(g_fin_mk->raw());
|
||||
g_funext = new name{"funext"};
|
||||
mark_persistent(g_funext->raw());
|
||||
g_has_add = new name{"HasAdd"};
|
||||
mark_persistent(g_has_add->raw());
|
||||
g_has_add_add = new name{"HasAdd", "add"};
|
||||
mark_persistent(g_has_add_add->raw());
|
||||
g_has_div_div = new name{"HasDiv", "div"};
|
||||
mark_persistent(g_has_div_div->raw());
|
||||
g_has_emptyc_emptyc = new name{"HasEmptyc", "emptyc"};
|
||||
mark_persistent(g_has_emptyc_emptyc->raw());
|
||||
g_has_insert_insert = new name{"HasInsert", "insert"};
|
||||
mark_persistent(g_has_insert_insert->raw());
|
||||
g_has_neg_neg = new name{"HasNeg", "neg"};
|
||||
mark_persistent(g_has_neg_neg->raw());
|
||||
g_has_one = new name{"HasOne"};
|
||||
mark_persistent(g_has_one->raw());
|
||||
g_has_one_one = new name{"HasOne", "one"};
|
||||
mark_persistent(g_has_one_one->raw());
|
||||
g_has_sep_sep = new name{"HasSep", "sep"};
|
||||
mark_persistent(g_has_sep_sep->raw());
|
||||
g_has_sub_sub = new name{"HasSub", "sub"};
|
||||
mark_persistent(g_has_sub_sub->raw());
|
||||
g_has_well_founded = new name{"HasWellFounded"};
|
||||
mark_persistent(g_has_well_founded->raw());
|
||||
g_has_well_founded_r = new name{"HasWellFounded", "r"};
|
||||
mark_persistent(g_has_well_founded_r->raw());
|
||||
g_has_well_founded_wf = new name{"HasWellFounded", "wf"};
|
||||
mark_persistent(g_has_well_founded_wf->raw());
|
||||
g_has_zero = new name{"HasZero"};
|
||||
mark_persistent(g_has_zero->raw());
|
||||
g_has_zero_zero = new name{"HasZero", "zero"};
|
||||
mark_persistent(g_has_zero_zero->raw());
|
||||
g_has_coe_t = new name{"HasCoeT"};
|
||||
mark_persistent(g_has_coe_t->raw());
|
||||
g_heq = new name{"HEq"};
|
||||
mark_persistent(g_heq->raw());
|
||||
g_heq_refl = new name{"HEq", "refl"};
|
||||
mark_persistent(g_heq_refl->raw());
|
||||
g_heq_symm = new name{"HEq", "symm"};
|
||||
mark_persistent(g_heq_symm->raw());
|
||||
g_heq_trans = new name{"HEq", "trans"};
|
||||
mark_persistent(g_heq_trans->raw());
|
||||
g_heq_of_eq = new name{"heqOfEq"};
|
||||
mark_persistent(g_heq_of_eq->raw());
|
||||
g_huge_fuel = new name{"hugeFuel"};
|
||||
mark_persistent(g_huge_fuel->raw());
|
||||
g_id = new name{"id"};
|
||||
mark_persistent(g_id->raw());
|
||||
g_id_rhs = new name{"idRhs"};
|
||||
mark_persistent(g_id_rhs->raw());
|
||||
g_id_delta = new name{"idDelta"};
|
||||
mark_persistent(g_id_delta->raw());
|
||||
g_iff_false_intro = new name{"iffFalseIntro"};
|
||||
mark_persistent(g_iff_false_intro->raw());
|
||||
g_iff = new name{"Iff"};
|
||||
mark_persistent(g_iff->raw());
|
||||
g_iff_mp = new name{"Iff", "mp"};
|
||||
mark_persistent(g_iff_mp->raw());
|
||||
g_iff_mpr = new name{"Iff", "mpr"};
|
||||
mark_persistent(g_iff_mpr->raw());
|
||||
g_iff_refl = new name{"Iff", "refl"};
|
||||
mark_persistent(g_iff_refl->raw());
|
||||
g_iff_symm = new name{"Iff", "symm"};
|
||||
mark_persistent(g_iff_symm->raw());
|
||||
g_iff_trans = new name{"Iff", "trans"};
|
||||
mark_persistent(g_iff_trans->raw());
|
||||
g_iff_true_intro = new name{"iffTrueIntro"};
|
||||
mark_persistent(g_iff_true_intro->raw());
|
||||
g_inhabited = new name{"Inhabited"};
|
||||
mark_persistent(g_inhabited->raw());
|
||||
g_inhabited_default = new name{"Inhabited", "default"};
|
||||
mark_persistent(g_inhabited_default->raw());
|
||||
g_int = new name{"Int"};
|
||||
mark_persistent(g_int->raw());
|
||||
g_int_nat_abs = new name{"Int", "natAbs"};
|
||||
mark_persistent(g_int_nat_abs->raw());
|
||||
g_int_dec_lt = new name{"Int", "decLt"};
|
||||
mark_persistent(g_int_dec_lt->raw());
|
||||
g_int_of_nat = new name{"Int", "ofNat"};
|
||||
mark_persistent(g_int_of_nat->raw());
|
||||
g_inline = new name{"inline"};
|
||||
mark_persistent(g_inline->raw());
|
||||
g_eio = new name{"EIO"};
|
||||
mark_persistent(g_eio->raw());
|
||||
g_st = new name{"ST"};
|
||||
mark_persistent(g_st->raw());
|
||||
g_io = new name{"IO"};
|
||||
mark_persistent(g_io->raw());
|
||||
g_ite = new name{"ite"};
|
||||
mark_persistent(g_ite->raw());
|
||||
g_lc_proof = new name{"lcProof"};
|
||||
mark_persistent(g_lc_proof->raw());
|
||||
g_lc_unreachable = new name{"lcUnreachable"};
|
||||
mark_persistent(g_lc_unreachable->raw());
|
||||
g_list = new name{"List"};
|
||||
mark_persistent(g_list->raw());
|
||||
g_list_nil = new name{"List", "nil"};
|
||||
mark_persistent(g_list_nil->raw());
|
||||
g_list_cons = new name{"List", "cons"};
|
||||
mark_persistent(g_list_cons->raw());
|
||||
g_list_to_array = new name{"List", "toArray"};
|
||||
mark_persistent(g_list_to_array->raw());
|
||||
g_monad = new name{"Monad"};
|
||||
mark_persistent(g_monad->raw());
|
||||
g_lean_name_anonymous = new name{"Lean", "Name", "anonymous"};
|
||||
mark_persistent(g_lean_name_anonymous->raw());
|
||||
g_lean_name_num = new name{"Lean", "Name", "num"};
|
||||
mark_persistent(g_lean_name_num->raw());
|
||||
g_lean_name_str = new name{"Lean", "Name", "str"};
|
||||
mark_persistent(g_lean_name_str->raw());
|
||||
g_lean_mk_name_num = new name{"Lean", "mkNameNum"};
|
||||
mark_persistent(g_lean_mk_name_num->raw());
|
||||
g_lean_mk_name_str = new name{"Lean", "mkNameStr"};
|
||||
mark_persistent(g_lean_mk_name_str->raw());
|
||||
g_lean_parser_leading_node = new name{"Lean", "Parser", "leadingNode"};
|
||||
mark_persistent(g_lean_parser_leading_node->raw());
|
||||
g_lean_parser_trailing_node = new name{"Lean", "Parser", "trailingNode"};
|
||||
mark_persistent(g_lean_parser_trailing_node->raw());
|
||||
g_mut_quot = new name{"MutQuot"};
|
||||
mark_persistent(g_mut_quot->raw());
|
||||
g_nat = new name{"Nat"};
|
||||
mark_persistent(g_nat->raw());
|
||||
g_nat_succ = new name{"Nat", "succ"};
|
||||
mark_persistent(g_nat_succ->raw());
|
||||
g_nat_zero = new name{"Nat", "zero"};
|
||||
mark_persistent(g_nat_zero->raw());
|
||||
g_nat_has_zero = new name{"Nat", "HasZero"};
|
||||
mark_persistent(g_nat_has_zero->raw());
|
||||
g_nat_has_one = new name{"Nat", "HasOne"};
|
||||
mark_persistent(g_nat_has_one->raw());
|
||||
g_nat_has_add = new name{"Nat", "HasAdd"};
|
||||
mark_persistent(g_nat_has_add->raw());
|
||||
g_nat_add = new name{"Nat", "add"};
|
||||
mark_persistent(g_nat_add->raw());
|
||||
g_nat_dec_eq = new name{"Nat", "decEq"};
|
||||
mark_persistent(g_nat_dec_eq->raw());
|
||||
g_nat_sub = new name{"Nat", "sub"};
|
||||
mark_persistent(g_nat_sub->raw());
|
||||
g_ne = new name{"ne"};
|
||||
mark_persistent(g_ne->raw());
|
||||
g_neq_of_not_iff = new name{"neqOfNotIff"};
|
||||
mark_persistent(g_neq_of_not_iff->raw());
|
||||
g_not = new name{"Not"};
|
||||
mark_persistent(g_not->raw());
|
||||
g_not_of_iff_false = new name{"notOfIffFalse"};
|
||||
mark_persistent(g_not_of_iff_false->raw());
|
||||
g_not_of_eq_false = new name{"notOfEqFalse"};
|
||||
mark_persistent(g_not_of_eq_false->raw());
|
||||
g_of_eq_true = new name{"ofEqTrue"};
|
||||
mark_persistent(g_of_eq_true->raw());
|
||||
g_of_iff_true = new name{"ofIffTrue"};
|
||||
mark_persistent(g_of_iff_true->raw());
|
||||
g_opt_param = new name{"optParam"};
|
||||
mark_persistent(g_opt_param->raw());
|
||||
g_or = new name{"Or"};
|
||||
mark_persistent(g_or->raw());
|
||||
g_panic = new name{"panic"};
|
||||
mark_persistent(g_panic->raw());
|
||||
g_panic_with_pos = new name{"panicWithPos"};
|
||||
mark_persistent(g_panic_with_pos->raw());
|
||||
g_punit = new name{"PUnit"};
|
||||
mark_persistent(g_punit->raw());
|
||||
g_punit_unit = new name{"PUnit", "unit"};
|
||||
mark_persistent(g_punit_unit->raw());
|
||||
g_prod_mk = new name{"Prod", "mk"};
|
||||
mark_persistent(g_prod_mk->raw());
|
||||
g_pprod = new name{"PProd"};
|
||||
mark_persistent(g_pprod->raw());
|
||||
g_pprod_mk = new name{"PProd", "mk"};
|
||||
mark_persistent(g_pprod_mk->raw());
|
||||
g_pprod_fst = new name{"PProd", "fst"};
|
||||
mark_persistent(g_pprod_fst->raw());
|
||||
g_pprod_snd = new name{"PProd", "snd"};
|
||||
mark_persistent(g_pprod_snd->raw());
|
||||
g_propext = new name{"propext"};
|
||||
mark_persistent(g_propext->raw());
|
||||
g_quot_mk = new name{"Quot", "mk"};
|
||||
mark_persistent(g_quot_mk->raw());
|
||||
g_quot_lift = new name{"Quot", "lift"};
|
||||
mark_persistent(g_quot_lift->raw());
|
||||
g_rfl = new name{"rfl"};
|
||||
mark_persistent(g_rfl->raw());
|
||||
g_scope_trace = new name{"scopeTrace"};
|
||||
mark_persistent(g_scope_trace->raw());
|
||||
g_set_of = new name{"setOf"};
|
||||
mark_persistent(g_set_of->raw());
|
||||
g_psigma = new name{"PSigma"};
|
||||
mark_persistent(g_psigma->raw());
|
||||
g_psigma_mk = new name{"PSigma", "mk"};
|
||||
mark_persistent(g_psigma_mk->raw());
|
||||
g_psigma_fst = new name{"PSigma", "fst"};
|
||||
mark_persistent(g_psigma_fst->raw());
|
||||
g_psigma_snd = new name{"PSigma", "snd"};
|
||||
mark_persistent(g_psigma_snd->raw());
|
||||
g_singleton = new name{"singleton"};
|
||||
mark_persistent(g_singleton->raw());
|
||||
g_sorry_ax = new name{"sorryAx"};
|
||||
mark_persistent(g_sorry_ax->raw());
|
||||
g_string = new name{"String"};
|
||||
mark_persistent(g_string->raw());
|
||||
g_string_data = new name{"String", "data"};
|
||||
mark_persistent(g_string_data->raw());
|
||||
g_string_empty = new name{"String", "Empty"};
|
||||
mark_persistent(g_string_empty->raw());
|
||||
g_string_str = new name{"String", "str"};
|
||||
mark_persistent(g_string_str->raw());
|
||||
g_subsingleton = new name{"subsingleton"};
|
||||
mark_persistent(g_subsingleton->raw());
|
||||
g_subsingleton_elim = new name{"subsingleton", "elim"};
|
||||
mark_persistent(g_subsingleton_elim->raw());
|
||||
g_subtype = new name{"Subtype"};
|
||||
mark_persistent(g_subtype->raw());
|
||||
g_psum = new name{"PSum"};
|
||||
mark_persistent(g_psum->raw());
|
||||
g_psum_cases_on = new name{"PSum", "casesOn"};
|
||||
mark_persistent(g_psum_cases_on->raw());
|
||||
g_psum_inl = new name{"PSum", "inl"};
|
||||
mark_persistent(g_psum_inl->raw());
|
||||
g_psum_inr = new name{"PSum", "inr"};
|
||||
mark_persistent(g_psum_inr->raw());
|
||||
g_subsingleton_elim = new name{"Subsingleton", "elim"};
|
||||
g_task = new name{"Task"};
|
||||
mark_persistent(g_task->raw());
|
||||
g_thunk = new name{"Thunk"};
|
||||
mark_persistent(g_thunk->raw());
|
||||
g_thunk_mk = new name{"Thunk", "mk"};
|
||||
mark_persistent(g_thunk_mk->raw());
|
||||
g_thunk_get = new name{"Thunk", "get"};
|
||||
mark_persistent(g_thunk_get->raw());
|
||||
g_true = new name{"True"};
|
||||
mark_persistent(g_true->raw());
|
||||
g_true_intro = new name{"True", "intro"};
|
||||
mark_persistent(g_true_intro->raw());
|
||||
g_typed_expr = new name{"typedExpr"};
|
||||
mark_persistent(g_typed_expr->raw());
|
||||
g_unit = new name{"Unit"};
|
||||
mark_persistent(g_unit->raw());
|
||||
g_unit_unit = new name{"Unit", "unit"};
|
||||
mark_persistent(g_unit_unit->raw());
|
||||
g_uint8 = new name{"UInt8"};
|
||||
mark_persistent(g_uint8->raw());
|
||||
g_uint16 = new name{"UInt16"};
|
||||
mark_persistent(g_uint16->raw());
|
||||
g_uint32 = new name{"UInt32"};
|
||||
mark_persistent(g_uint32->raw());
|
||||
g_uint64 = new name{"UInt64"};
|
||||
mark_persistent(g_uint64->raw());
|
||||
g_usize = new name{"USize"};
|
||||
mark_persistent(g_usize->raw());
|
||||
g_well_founded_fix = new name{"WellFounded", "fix"};
|
||||
mark_persistent(g_well_founded_fix->raw());
|
||||
g_well_founded_tactics = new name{"wellFoundedTactics"};
|
||||
mark_persistent(g_well_founded_tactics->raw());
|
||||
g_well_founded_tactics_default = new name{"wellFoundedTactics", "default"};
|
||||
mark_persistent(g_well_founded_tactics_default->raw());
|
||||
g_well_founded_tactics_rel_tac = new name{"wellFoundedTactics", "relTac"};
|
||||
mark_persistent(g_well_founded_tactics_rel_tac->raw());
|
||||
g_well_founded_tactics_dec_tac = new name{"wellFoundedTactics", "decTac"};
|
||||
mark_persistent(g_well_founded_tactics_dec_tac->raw());
|
||||
}
|
||||
void finalize_constants() {
|
||||
delete g_absurd;
|
||||
|
|
@ -606,20 +233,11 @@ void finalize_constants() {
|
|||
delete g_bool_cases_on;
|
||||
delete g_cast;
|
||||
delete g_char;
|
||||
delete g_char_mk;
|
||||
delete g_char_of_nat;
|
||||
delete g_old_coe;
|
||||
delete g_old_coe_fn;
|
||||
delete g_old_coe_sort;
|
||||
delete g_old_coe_to_lift;
|
||||
delete g_congr;
|
||||
delete g_congr_arg;
|
||||
delete g_congr_fun;
|
||||
delete g_decidable;
|
||||
delete g_decidable_is_true;
|
||||
delete g_decidable_is_false;
|
||||
delete g_decidable_decide;
|
||||
delete g_dite;
|
||||
delete g_empty;
|
||||
delete g_empty_rec;
|
||||
delete g_empty_cases_on;
|
||||
|
|
@ -628,86 +246,34 @@ void finalize_constants() {
|
|||
delete g_eq_cases_on;
|
||||
delete g_eq_rec_on;
|
||||
delete g_eq_rec;
|
||||
delete g_eq_mp;
|
||||
delete g_eq_mpr;
|
||||
delete g_eq_ndrec;
|
||||
delete g_eq_refl;
|
||||
delete g_eq_subst;
|
||||
delete g_eq_symm;
|
||||
delete g_eq_trans;
|
||||
delete g_eq_of_heq;
|
||||
delete g_eq_true_intro;
|
||||
delete g_eq_false_intro;
|
||||
delete g_eq_self_iff_true;
|
||||
delete g_float;
|
||||
delete g_float_array;
|
||||
delete g_lean_message_data;
|
||||
delete g_lean_monad_tracer_trace;
|
||||
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_funext;
|
||||
delete g_has_add;
|
||||
delete g_has_add_add;
|
||||
delete g_has_div_div;
|
||||
delete g_has_emptyc_emptyc;
|
||||
delete g_has_insert_insert;
|
||||
delete g_has_neg_neg;
|
||||
delete g_has_one;
|
||||
delete g_has_one_one;
|
||||
delete g_has_sep_sep;
|
||||
delete g_has_sub_sub;
|
||||
delete g_has_well_founded;
|
||||
delete g_has_well_founded_r;
|
||||
delete g_has_well_founded_wf;
|
||||
delete g_has_zero;
|
||||
delete g_has_zero_zero;
|
||||
delete g_has_coe_t;
|
||||
delete g_heq;
|
||||
delete g_heq_refl;
|
||||
delete g_heq_symm;
|
||||
delete g_heq_trans;
|
||||
delete g_heq_of_eq;
|
||||
delete g_huge_fuel;
|
||||
delete g_id;
|
||||
delete g_id_rhs;
|
||||
delete g_id_delta;
|
||||
delete g_iff_false_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_inhabited;
|
||||
delete g_inhabited_default;
|
||||
delete g_int;
|
||||
delete g_int_nat_abs;
|
||||
delete g_int_dec_lt;
|
||||
delete g_int_of_nat;
|
||||
delete g_inline;
|
||||
delete g_eio;
|
||||
delete g_st;
|
||||
delete g_io;
|
||||
delete g_ite;
|
||||
delete g_lc_proof;
|
||||
delete g_lc_unreachable;
|
||||
delete g_list;
|
||||
delete g_list_nil;
|
||||
delete g_list_cons;
|
||||
delete g_list_to_array;
|
||||
delete g_monad;
|
||||
delete g_lean_name_anonymous;
|
||||
delete g_lean_name_num;
|
||||
delete g_lean_name_str;
|
||||
delete g_lean_mk_name_num;
|
||||
delete g_lean_mk_name_str;
|
||||
delete g_lean_parser_leading_node;
|
||||
delete g_lean_parser_trailing_node;
|
||||
delete g_mut_quot;
|
||||
delete g_nat;
|
||||
delete g_nat_succ;
|
||||
|
|
@ -719,19 +285,12 @@ void finalize_constants() {
|
|||
delete g_nat_dec_eq;
|
||||
delete g_nat_sub;
|
||||
delete g_ne;
|
||||
delete g_neq_of_not_iff;
|
||||
delete g_not;
|
||||
delete g_not_of_iff_false;
|
||||
delete g_not_of_eq_false;
|
||||
delete g_of_eq_true;
|
||||
delete g_of_iff_true;
|
||||
delete g_opt_param;
|
||||
delete g_or;
|
||||
delete g_panic;
|
||||
delete g_panic_with_pos;
|
||||
delete g_punit;
|
||||
delete g_punit_unit;
|
||||
delete g_prod_mk;
|
||||
delete g_pprod;
|
||||
delete g_pprod_mk;
|
||||
delete g_pprod_fst;
|
||||
|
|
@ -739,33 +298,16 @@ void finalize_constants() {
|
|||
delete g_propext;
|
||||
delete g_quot_mk;
|
||||
delete g_quot_lift;
|
||||
delete g_rfl;
|
||||
delete g_scope_trace;
|
||||
delete g_set_of;
|
||||
delete g_psigma;
|
||||
delete g_psigma_mk;
|
||||
delete g_psigma_fst;
|
||||
delete g_psigma_snd;
|
||||
delete g_singleton;
|
||||
delete g_sorry_ax;
|
||||
delete g_string;
|
||||
delete g_string_data;
|
||||
delete g_string_empty;
|
||||
delete g_string_str;
|
||||
delete g_subsingleton;
|
||||
delete g_subsingleton_elim;
|
||||
delete g_subtype;
|
||||
delete g_psum;
|
||||
delete g_psum_cases_on;
|
||||
delete g_psum_inl;
|
||||
delete g_psum_inr;
|
||||
delete g_task;
|
||||
delete g_thunk;
|
||||
delete g_thunk_mk;
|
||||
delete g_thunk_get;
|
||||
delete g_true;
|
||||
delete g_true_intro;
|
||||
delete g_typed_expr;
|
||||
delete g_unit;
|
||||
delete g_unit_unit;
|
||||
delete g_uint8;
|
||||
|
|
@ -773,11 +315,6 @@ void finalize_constants() {
|
|||
delete g_uint32;
|
||||
delete g_uint64;
|
||||
delete g_usize;
|
||||
delete g_well_founded_fix;
|
||||
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;
|
||||
}
|
||||
name const & get_absurd_name() { return *g_absurd; }
|
||||
name const & get_and_name() { return *g_and; }
|
||||
|
|
@ -800,20 +337,11 @@ name const & get_bool_true_name() { return *g_bool_true; }
|
|||
name const & get_bool_cases_on_name() { return *g_bool_cases_on; }
|
||||
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_of_nat_name() { return *g_char_of_nat; }
|
||||
name const & get_old_coe_name() { return *g_old_coe; }
|
||||
name const & get_old_coe_fn_name() { return *g_old_coe_fn; }
|
||||
name const & get_old_coe_sort_name() { return *g_old_coe_sort; }
|
||||
name const & get_old_coe_to_lift_name() { return *g_old_coe_to_lift; }
|
||||
name const & get_congr_name() { return *g_congr; }
|
||||
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_is_true_name() { return *g_decidable_is_true; }
|
||||
name const & get_decidable_is_false_name() { return *g_decidable_is_false; }
|
||||
name const & get_decidable_decide_name() { return *g_decidable_decide; }
|
||||
name const & get_dite_name() { return *g_dite; }
|
||||
name const & get_empty_name() { return *g_empty; }
|
||||
name const & get_empty_rec_name() { return *g_empty_rec; }
|
||||
name const & get_empty_cases_on_name() { return *g_empty_cases_on; }
|
||||
|
|
@ -822,86 +350,34 @@ name const & get_eq_name() { return *g_eq; }
|
|||
name const & get_eq_cases_on_name() { return *g_eq_cases_on; }
|
||||
name const & get_eq_rec_on_name() { return *g_eq_rec_on; }
|
||||
name const & get_eq_rec_name() { return *g_eq_rec; }
|
||||
name const & get_eq_mp_name() { return *g_eq_mp; }
|
||||
name const & get_eq_mpr_name() { return *g_eq_mpr; }
|
||||
name const & get_eq_ndrec_name() { return *g_eq_ndrec; }
|
||||
name const & get_eq_refl_name() { return *g_eq_refl; }
|
||||
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_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_float_name() { return *g_float; }
|
||||
name const & get_float_array_name() { return *g_float_array; }
|
||||
name const & get_lean_message_data_name() { return *g_lean_message_data; }
|
||||
name const & get_lean_monad_tracer_trace_name() { return *g_lean_monad_tracer_trace; }
|
||||
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_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_div_div_name() { return *g_has_div_div; }
|
||||
name const & get_has_emptyc_emptyc_name() { return *g_has_emptyc_emptyc; }
|
||||
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_sep_sep_name() { return *g_has_sep_sep; }
|
||||
name const & get_has_sub_sub_name() { return *g_has_sub_sub; }
|
||||
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; }
|
||||
name const & get_has_well_founded_wf_name() { return *g_has_well_founded_wf; }
|
||||
name const & get_has_zero_name() { return *g_has_zero; }
|
||||
name const & get_has_zero_zero_name() { return *g_has_zero_zero; }
|
||||
name const & get_has_coe_t_name() { return *g_has_coe_t; }
|
||||
name const & get_heq_name() { return *g_heq; }
|
||||
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_huge_fuel_name() { return *g_huge_fuel; }
|
||||
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_iff_false_intro_name() { return *g_iff_false_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_inhabited_name() { return *g_inhabited; }
|
||||
name const & get_inhabited_default_name() { return *g_inhabited_default; }
|
||||
name const & get_int_name() { return *g_int; }
|
||||
name const & get_int_nat_abs_name() { return *g_int_nat_abs; }
|
||||
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_inline_name() { return *g_inline; }
|
||||
name const & get_eio_name() { return *g_eio; }
|
||||
name const & get_st_name() { return *g_st; }
|
||||
name const & get_io_name() { return *g_io; }
|
||||
name const & get_ite_name() { return *g_ite; }
|
||||
name const & get_lc_proof_name() { return *g_lc_proof; }
|
||||
name const & get_lc_unreachable_name() { return *g_lc_unreachable; }
|
||||
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_list_to_array_name() { return *g_list_to_array; }
|
||||
name const & get_monad_name() { return *g_monad; }
|
||||
name const & get_lean_name_anonymous_name() { return *g_lean_name_anonymous; }
|
||||
name const & get_lean_name_num_name() { return *g_lean_name_num; }
|
||||
name const & get_lean_name_str_name() { return *g_lean_name_str; }
|
||||
name const & get_lean_mk_name_num_name() { return *g_lean_mk_name_num; }
|
||||
name const & get_lean_mk_name_str_name() { return *g_lean_mk_name_str; }
|
||||
name const & get_lean_parser_leading_node_name() { return *g_lean_parser_leading_node; }
|
||||
name const & get_lean_parser_trailing_node_name() { return *g_lean_parser_trailing_node; }
|
||||
name const & get_mut_quot_name() { return *g_mut_quot; }
|
||||
name const & get_nat_name() { return *g_nat; }
|
||||
name const & get_nat_succ_name() { return *g_nat_succ; }
|
||||
|
|
@ -913,19 +389,12 @@ name const & get_nat_add_name() { return *g_nat_add; }
|
|||
name const & get_nat_dec_eq_name() { return *g_nat_dec_eq; }
|
||||
name const & get_nat_sub_name() { return *g_nat_sub; }
|
||||
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; }
|
||||
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; }
|
||||
name const & get_of_eq_true_name() { return *g_of_eq_true; }
|
||||
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_panic_name() { return *g_panic; }
|
||||
name const & get_panic_with_pos_name() { return *g_panic_with_pos; }
|
||||
name const & get_punit_name() { return *g_punit; }
|
||||
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; }
|
||||
name const & get_pprod_mk_name() { return *g_pprod_mk; }
|
||||
name const & get_pprod_fst_name() { return *g_pprod_fst; }
|
||||
|
|
@ -933,33 +402,16 @@ name const & get_pprod_snd_name() { return *g_pprod_snd; }
|
|||
name const & get_propext_name() { return *g_propext; }
|
||||
name const & get_quot_mk_name() { return *g_quot_mk; }
|
||||
name const & get_quot_lift_name() { return *g_quot_lift; }
|
||||
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_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_sorry_ax_name() { return *g_sorry_ax; }
|
||||
name const & get_string_name() { return *g_string; }
|
||||
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_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_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_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_thunk_get_name() { return *g_thunk_get; }
|
||||
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_uint8_name() { return *g_uint8; }
|
||||
|
|
@ -967,9 +419,4 @@ 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_well_founded_fix_name() { return *g_well_founded_fix; }
|
||||
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; }
|
||||
}
|
||||
|
|
|
|||
|
|
@ -26,20 +26,11 @@ name const & get_bool_true_name();
|
|||
name const & get_bool_cases_on_name();
|
||||
name const & get_cast_name();
|
||||
name const & get_char_name();
|
||||
name const & get_char_mk_name();
|
||||
name const & get_char_of_nat_name();
|
||||
name const & get_old_coe_name();
|
||||
name const & get_old_coe_fn_name();
|
||||
name const & get_old_coe_sort_name();
|
||||
name const & get_old_coe_to_lift_name();
|
||||
name const & get_congr_name();
|
||||
name const & get_congr_arg_name();
|
||||
name const & get_congr_fun_name();
|
||||
name const & get_decidable_name();
|
||||
name const & get_decidable_is_true_name();
|
||||
name const & get_decidable_is_false_name();
|
||||
name const & get_decidable_decide_name();
|
||||
name const & get_dite_name();
|
||||
name const & get_empty_name();
|
||||
name const & get_empty_rec_name();
|
||||
name const & get_empty_cases_on_name();
|
||||
|
|
@ -48,86 +39,34 @@ name const & get_eq_name();
|
|||
name const & get_eq_cases_on_name();
|
||||
name const & get_eq_rec_on_name();
|
||||
name const & get_eq_rec_name();
|
||||
name const & get_eq_mp_name();
|
||||
name const & get_eq_mpr_name();
|
||||
name const & get_eq_ndrec_name();
|
||||
name const & get_eq_refl_name();
|
||||
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_true_intro_name();
|
||||
name const & get_eq_false_intro_name();
|
||||
name const & get_eq_self_iff_true_name();
|
||||
name const & get_float_name();
|
||||
name const & get_float_array_name();
|
||||
name const & get_lean_message_data_name();
|
||||
name const & get_lean_monad_tracer_trace_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_funext_name();
|
||||
name const & get_has_add_name();
|
||||
name const & get_has_add_add_name();
|
||||
name const & get_has_div_div_name();
|
||||
name const & get_has_emptyc_emptyc_name();
|
||||
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_sep_sep_name();
|
||||
name const & get_has_sub_sub_name();
|
||||
name const & get_has_well_founded_name();
|
||||
name const & get_has_well_founded_r_name();
|
||||
name const & get_has_well_founded_wf_name();
|
||||
name const & get_has_zero_name();
|
||||
name const & get_has_zero_zero_name();
|
||||
name const & get_has_coe_t_name();
|
||||
name const & get_heq_name();
|
||||
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_huge_fuel_name();
|
||||
name const & get_id_name();
|
||||
name const & get_id_rhs_name();
|
||||
name const & get_id_delta_name();
|
||||
name const & get_iff_false_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_inhabited_name();
|
||||
name const & get_inhabited_default_name();
|
||||
name const & get_int_name();
|
||||
name const & get_int_nat_abs_name();
|
||||
name const & get_int_dec_lt_name();
|
||||
name const & get_int_of_nat_name();
|
||||
name const & get_inline_name();
|
||||
name const & get_eio_name();
|
||||
name const & get_st_name();
|
||||
name const & get_io_name();
|
||||
name const & get_ite_name();
|
||||
name const & get_lc_proof_name();
|
||||
name const & get_lc_unreachable_name();
|
||||
name const & get_list_name();
|
||||
name const & get_list_nil_name();
|
||||
name const & get_list_cons_name();
|
||||
name const & get_list_to_array_name();
|
||||
name const & get_monad_name();
|
||||
name const & get_lean_name_anonymous_name();
|
||||
name const & get_lean_name_num_name();
|
||||
name const & get_lean_name_str_name();
|
||||
name const & get_lean_mk_name_num_name();
|
||||
name const & get_lean_mk_name_str_name();
|
||||
name const & get_lean_parser_leading_node_name();
|
||||
name const & get_lean_parser_trailing_node_name();
|
||||
name const & get_mut_quot_name();
|
||||
name const & get_nat_name();
|
||||
name const & get_nat_succ_name();
|
||||
|
|
@ -139,19 +78,12 @@ name const & get_nat_add_name();
|
|||
name const & get_nat_dec_eq_name();
|
||||
name const & get_nat_sub_name();
|
||||
name const & get_ne_name();
|
||||
name const & get_neq_of_not_iff_name();
|
||||
name const & get_not_name();
|
||||
name const & get_not_of_iff_false_name();
|
||||
name const & get_not_of_eq_false_name();
|
||||
name const & get_of_eq_true_name();
|
||||
name const & get_of_iff_true_name();
|
||||
name const & get_opt_param_name();
|
||||
name const & get_or_name();
|
||||
name const & get_panic_name();
|
||||
name const & get_panic_with_pos_name();
|
||||
name const & get_punit_name();
|
||||
name const & get_punit_unit_name();
|
||||
name const & get_prod_mk_name();
|
||||
name const & get_pprod_name();
|
||||
name const & get_pprod_mk_name();
|
||||
name const & get_pprod_fst_name();
|
||||
|
|
@ -159,33 +91,16 @@ name const & get_pprod_snd_name();
|
|||
name const & get_propext_name();
|
||||
name const & get_quot_mk_name();
|
||||
name const & get_quot_lift_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_mk_name();
|
||||
name const & get_psigma_fst_name();
|
||||
name const & get_psigma_snd_name();
|
||||
name const & get_singleton_name();
|
||||
name const & get_sorry_ax_name();
|
||||
name const & get_string_name();
|
||||
name const & get_string_data_name();
|
||||
name const & get_string_empty_name();
|
||||
name const & get_string_str_name();
|
||||
name const & get_subsingleton_name();
|
||||
name const & get_subsingleton_elim_name();
|
||||
name const & get_subtype_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_task_name();
|
||||
name const & get_thunk_name();
|
||||
name const & get_thunk_mk_name();
|
||||
name const & get_thunk_get_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_uint8_name();
|
||||
|
|
@ -193,9 +108,4 @@ name const & get_uint16_name();
|
|||
name const & get_uint32_name();
|
||||
name const & get_uint64_name();
|
||||
name const & get_usize_name();
|
||||
name const & get_well_founded_fix_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();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -19,20 +19,11 @@ Bool.true
|
|||
Bool.casesOn
|
||||
cast
|
||||
Char
|
||||
Char.mk
|
||||
Char.ofNat
|
||||
oldCoe
|
||||
oldCoeFn
|
||||
oldCoeSort
|
||||
oldCoeToLift
|
||||
congr
|
||||
congrArg
|
||||
congrFun
|
||||
Decidable
|
||||
Decidable.isTrue
|
||||
Decidable.isFalse
|
||||
Decidable.decide
|
||||
dite
|
||||
Empty
|
||||
Empty.rec
|
||||
Empty.casesOn
|
||||
|
|
@ -41,86 +32,34 @@ Eq
|
|||
Eq.casesOn
|
||||
Eq.recOn
|
||||
Eq.rec
|
||||
Eq.mp
|
||||
Eq.mpr
|
||||
Eq.ndrec
|
||||
Eq.refl
|
||||
Eq.subst
|
||||
Eq.symm
|
||||
Eq.trans
|
||||
eqOfHEq
|
||||
eqTrueIntro
|
||||
eqFalseIntro
|
||||
eqSelfIffTrue
|
||||
Float
|
||||
FloatArray
|
||||
Lean.MessageData
|
||||
Lean.MonadTracer.trace
|
||||
False
|
||||
falseOfTrueIffFalse
|
||||
falseOfTrueEqFalse
|
||||
False.rec
|
||||
False.casesOn
|
||||
Fin.mk
|
||||
funext
|
||||
HasAdd
|
||||
HasAdd.add
|
||||
HasDiv.div
|
||||
HasEmptyc.emptyc
|
||||
HasInsert.insert
|
||||
HasNeg.neg
|
||||
HasOne
|
||||
HasOne.one
|
||||
HasSep.sep
|
||||
HasSub.sub
|
||||
HasWellFounded
|
||||
HasWellFounded.r
|
||||
HasWellFounded.wf
|
||||
HasZero
|
||||
HasZero.zero
|
||||
HasCoeT
|
||||
HEq
|
||||
HEq.refl
|
||||
HEq.symm
|
||||
HEq.trans
|
||||
heqOfEq
|
||||
hugeFuel
|
||||
id
|
||||
idRhs
|
||||
idDelta
|
||||
iffFalseIntro
|
||||
Iff
|
||||
Iff.mp
|
||||
Iff.mpr
|
||||
Iff.refl
|
||||
Iff.symm
|
||||
Iff.trans
|
||||
iffTrueIntro
|
||||
Inhabited
|
||||
Inhabited.default
|
||||
Int
|
||||
Int.natAbs
|
||||
Int.decLt
|
||||
Int.ofNat
|
||||
inline
|
||||
EIO
|
||||
ST
|
||||
IO
|
||||
ite
|
||||
lcProof
|
||||
lcUnreachable
|
||||
List
|
||||
List.nil
|
||||
List.cons
|
||||
List.toArray
|
||||
Monad
|
||||
Lean.Name.anonymous
|
||||
Lean.Name.num
|
||||
Lean.Name.str
|
||||
Lean.mkNameNum
|
||||
Lean.mkNameStr
|
||||
Lean.Parser.leadingNode
|
||||
Lean.Parser.trailingNode
|
||||
MutQuot
|
||||
Nat
|
||||
Nat.succ
|
||||
|
|
@ -132,19 +71,12 @@ Nat.add
|
|||
Nat.decEq
|
||||
Nat.sub
|
||||
ne
|
||||
neqOfNotIff
|
||||
Not
|
||||
notOfIffFalse
|
||||
notOfEqFalse
|
||||
ofEqTrue
|
||||
ofIffTrue
|
||||
optParam
|
||||
Or
|
||||
panic
|
||||
panicWithPos
|
||||
PUnit
|
||||
PUnit.unit
|
||||
Prod.mk
|
||||
PProd
|
||||
PProd.mk
|
||||
PProd.fst
|
||||
|
|
@ -152,33 +84,16 @@ PProd.snd
|
|||
propext
|
||||
Quot.mk
|
||||
Quot.lift
|
||||
rfl
|
||||
scopeTrace
|
||||
setOf
|
||||
PSigma
|
||||
PSigma.mk
|
||||
PSigma.fst
|
||||
PSigma.snd
|
||||
singleton
|
||||
sorryAx
|
||||
String
|
||||
String.data
|
||||
String.Empty
|
||||
String.str
|
||||
subsingleton
|
||||
subsingleton.elim
|
||||
Subtype
|
||||
PSum
|
||||
PSum.casesOn
|
||||
PSum.inl
|
||||
PSum.inr
|
||||
Subsingleton.elim
|
||||
Task
|
||||
Thunk
|
||||
Thunk.mk
|
||||
Thunk.get
|
||||
True
|
||||
True.intro
|
||||
typedExpr
|
||||
Unit
|
||||
Unit.unit
|
||||
UInt8 uint8
|
||||
|
|
@ -186,8 +101,3 @@ UInt16 uint16
|
|||
UInt32 uint32
|
||||
UInt64 uint64
|
||||
USize usize
|
||||
WellFounded.fix
|
||||
wellFoundedTactics
|
||||
wellFoundedTactics.default
|
||||
wellFoundedTactics.relTac
|
||||
wellFoundedTactics.decTac
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue