From 95fba3dba603bc3ee0760b33e8f2408ef12b3cbd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 13 Dec 2015 21:39:45 -0800 Subject: [PATCH] chore(library/constants): sort constant decls --- src/library/constants.cpp | 560 +++++++++++++++++++------------------- src/library/constants.h | 140 +++++----- src/library/constants.txt | 140 +++++----- 3 files changed, 420 insertions(+), 420 deletions(-) diff --git a/src/library/constants.cpp b/src/library/constants.cpp index 940f7a6fc..8fa7f2573 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -7,8 +7,8 @@ name const * g_absurd = nullptr; name const * g_add = nullptr; name const * g_add_comm_group = nullptr; name const * g_add_comm_semigroup = nullptr; -name const * g_add_monoid = 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; @@ -32,145 +32,147 @@ name const * g_div = nullptr; name const * g_empty = nullptr; name const * g_empty_rec = nullptr; name const * g_eq = nullptr; +name const * g_eq_drec = nullptr; name const * g_eq_elim_inv_inv = nullptr; name const * g_eq_intro = nullptr; -name const * g_eq_rec = nullptr; -name const * g_eq_drec = nullptr; name const * g_eq_mp = nullptr; name const * g_eq_mpr = nullptr; name const * g_eq_nrec = nullptr; +name const * g_eq_rec = nullptr; name const * g_eq_rec_eq = 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_subst = nullptr; name const * g_exists_elim = nullptr; name const * g_false = nullptr; -name const * g_false_rec = nullptr; name const * g_false_of_true_iff_false = nullptr; +name const * g_false_rec = nullptr; name const * g_field = nullptr; name const * g_funext = nullptr; -name const * g_has_zero = nullptr; -name const * g_has_one = nullptr; -name const * g_has_zero_zero = nullptr; -name const * g_has_one_one = nullptr; name const * g_has_add = nullptr; name const * g_has_div = nullptr; name const * g_has_mul = nullptr; name const * g_has_neg = nullptr; +name const * g_has_one = nullptr; +name const * g_has_one_one = nullptr; name const * g_has_sub = nullptr; +name const * g_has_zero = nullptr; +name const * g_has_zero_zero = nullptr; name const * g_heq = nullptr; name const * g_heq_refl = nullptr; name const * g_heq_to_eq = nullptr; name const * g_iff = nullptr; -name const * g_iff_refl = nullptr; -name const * g_iff_symm = nullptr; -name const * g_iff_trans = nullptr; -name const * g_iff_mp = nullptr; -name const * g_iff_mpr = nullptr; -name const * g_iff_intro = nullptr; name const * g_iff_elim_left = nullptr; name const * g_iff_elim_right = nullptr; name const * g_iff_false_intro = nullptr; +name const * g_iff_intro = 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_implies_resolve = nullptr; name const * g_implies = nullptr; -name const * g_implies_of_if_pos = nullptr; name const * g_implies_of_if_neg = nullptr; +name const * g_implies_of_if_pos = nullptr; +name const * g_implies_resolve = nullptr; +name const * g_is_trunc_is_hprop = nullptr; name const * g_is_trunc_is_hprop_elim = nullptr; +name const * g_is_trunc_is_hset = nullptr; name const * g_ite = nullptr; -name const * g_le_refl = nullptr; name const * g_left_distrib = nullptr; -name const * g_linear_ordered_semiring = nullptr; -name const * g_linear_ordered_ring = nullptr; +name const * g_le_refl = nullptr; name const * g_lift = nullptr; name const * g_lift_down = nullptr; name const * g_lift_up = nullptr; +name const * g_linear_ordered_ring = nullptr; +name const * g_linear_ordered_semiring = nullptr; name const * g_monoid = nullptr; name const * g_mul = nullptr; name const * g_mul_one = nullptr; -name const * g_mul_zero_class = nullptr; name const * g_mul_zero = nullptr; +name const * g_mul_zero_class = nullptr; name const * g_nat = nullptr; name const * g_nat_of_num = nullptr; name const * g_nat_succ = nullptr; name const * g_nat_zero = nullptr; name const * g_ne = nullptr; name const * g_neg = nullptr; -name const * g_not = nullptr; -name const * g_not_of_iff_false = nullptr; -name const * g_not_of_not_not_not = 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_zero = 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_bit1_add_bit0_helper = nullptr; name const * g_norm_num_bit0_add_bit1_helper = nullptr; -name const * g_norm_num_bit1_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_one_add_bit1_helper = nullptr; -name const * g_norm_num_one_add_bit0 = nullptr; -name const * g_norm_num_one_add_one = nullptr; -name const * g_norm_num_subst_into_prod = nullptr; -name const * g_norm_num_subst_into_sum = nullptr; -name const * g_norm_num_subst_into_subtr = 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_pos_add_neg_helper = 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_pos_mul_neg_helper = nullptr; -name const * g_norm_num_sub_eq_add_neg_helper = nullptr; -name const * g_norm_num_pos_add_pos_helper = nullptr; name const * g_norm_num_neg_neg_helper = nullptr; -name const * g_norm_num_add_div_helper = nullptr; -name const * g_norm_num_div_add_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_pos_bit0_helper = nullptr; -name const * g_norm_num_pos_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_mul_div_helper = nullptr; -name const * g_norm_num_div_mul_helper = nullptr; -name const * g_norm_num_div_helper = nullptr; -name const * g_norm_num_div_eq_div_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_add_pos_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_eq_add_neg_helper = nullptr; name const * g_norm_num_subst_into_div = nullptr; -name const * g_norm_num_nonzero_of_div_helper = nullptr; -name const * g_norm_num_neg_zero_helper = 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_not_not_not = nullptr; name const * g_num = nullptr; -name const * g_num_zero = nullptr; name const * g_num_pos = nullptr; +name const * g_num_zero = nullptr; name const * g_of_iff_true = nullptr; name const * g_one = nullptr; name const * g_one_mul = nullptr; name const * g_option = nullptr; -name const * g_option_some = nullptr; name const * g_option_none = nullptr; +name const * g_option_some = nullptr; name const * g_or = nullptr; name const * g_or_elim = nullptr; name const * g_or_intro_left = nullptr; name const * g_or_intro_right = nullptr; +name const * g_or_neg_resolve_left = nullptr; +name const * g_or_neg_resolve_right = nullptr; name const * g_or_rec = nullptr; name const * g_or_resolve_left = nullptr; name const * g_or_resolve_right = nullptr; -name const * g_or_neg_resolve_left = nullptr; -name const * g_or_neg_resolve_right = nullptr; name const * g_poly_unit = nullptr; name const * g_poly_unit_star = nullptr; name const * g_pos_num = nullptr; -name const * g_pos_num_one = nullptr; name const * g_pos_num_bit0 = nullptr; name const * g_pos_num_bit1 = nullptr; +name const * g_pos_num_one = nullptr; name const * g_prod = nullptr; name const * g_prod_mk = nullptr; name const * g_prod_pr1 = nullptr; @@ -178,8 +180,8 @@ name const * g_prod_pr2 = nullptr; name const * g_propext = nullptr; name const * g_rat_divide = nullptr; name const * g_rat_of_num = nullptr; -name const * g_ring = nullptr; name const * g_right_distrib = nullptr; +name const * g_ring = nullptr; name const * g_semiring = nullptr; name const * g_sigma = nullptr; name const * g_sigma_mk = nullptr; @@ -192,13 +194,10 @@ name const * g_subsingleton = nullptr; name const * g_subsingleton_elim = nullptr; name const * g_tactic = nullptr; name const * g_tactic_all_goals = nullptr; -name const * g_tactic_apply = nullptr; -name const * g_tactic_assert_hypothesis = nullptr; -name const * g_tactic_eapply = nullptr; -name const * g_tactic_fapply = nullptr; -name const * g_tactic_eassumption = nullptr; name const * g_tactic_and_then = nullptr; name const * g_tactic_append = nullptr; +name const * g_tactic_apply = nullptr; +name const * g_tactic_assert_hypothesis = nullptr; name const * g_tactic_assumption = nullptr; name const * g_tactic_at_most = nullptr; name const * g_tactic_beta = nullptr; @@ -210,30 +209,32 @@ name const * g_tactic_clear = nullptr; name const * g_tactic_clears = nullptr; name const * g_tactic_determ = nullptr; name const * g_tactic_discard = nullptr; -name const * g_tactic_intro = nullptr; -name const * g_tactic_intros = nullptr; +name const * g_tactic_eapply = nullptr; +name const * g_tactic_eassumption = nullptr; name const * g_tactic_exact = nullptr; name const * g_tactic_expr = nullptr; name const * g_tactic_expr_builtin = nullptr; name const * g_tactic_expr_list = nullptr; name const * g_tactic_expr_list_cons = nullptr; name const * g_tactic_expr_list_nil = nullptr; -name const * g_tactic_using_expr = nullptr; -name const * g_tactic_none_expr = nullptr; -name const * g_tactic_identifier = nullptr; -name const * g_tactic_identifier_list = nullptr; -name const * g_tactic_opt_expr = nullptr; -name const * g_tactic_opt_identifier_list = nullptr; name const * g_tactic_fail = nullptr; +name const * g_tactic_fapply = nullptr; name const * g_tactic_fixpoint = nullptr; name const * g_tactic_focus_at = nullptr; -name const * g_tactic_generalize_tac = nullptr; name const * g_tactic_generalizes = nullptr; +name const * g_tactic_generalize_tac = nullptr; name const * g_tactic_id = nullptr; +name const * g_tactic_identifier = nullptr; +name const * g_tactic_identifier_list = nullptr; name const * g_tactic_interleave = nullptr; +name const * g_tactic_intro = nullptr; +name const * g_tactic_intros = nullptr; name const * g_tactic_lettac = nullptr; +name const * g_tactic_none_expr = nullptr; name const * g_tactic_now = nullptr; +name const * g_tactic_opt_expr = nullptr; name const * g_tactic_opt_expr_list = nullptr; +name const * g_tactic_opt_identifier_list = nullptr; name const * g_tactic_or_else = nullptr; name const * g_tactic_par = nullptr; name const * g_tactic_refine = nullptr; @@ -247,26 +248,25 @@ name const * g_tactic_rotate_right = nullptr; name const * g_tactic_state = nullptr; name const * g_tactic_trace = nullptr; name const * g_tactic_try_for = nullptr; +name const * g_tactic_using_expr = nullptr; name const * g_tactic_whnf = 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_is_trunc_is_hset = nullptr; -name const * g_is_trunc_is_hprop = nullptr; name const * g_weak_order = nullptr; name const * g_well_founded = nullptr; name const * g_zero = nullptr; -name const * g_zero_mul = 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_add = new name{"add"}; g_add_comm_group = new name{"add_comm_group"}; g_add_comm_semigroup = new name{"add_comm_semigroup"}; - g_add_monoid = new name{"add_monoid"}; 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"}; @@ -290,145 +290,147 @@ void initialize_constants() { g_empty = new name{"empty"}; g_empty_rec = new name{"empty", "rec"}; g_eq = new name{"eq"}; + g_eq_drec = new name{"eq", "drec"}; g_eq_elim_inv_inv = new name{"eq", "elim_inv_inv"}; g_eq_intro = new name{"eq", "intro"}; - g_eq_rec = new name{"eq", "rec"}; - g_eq_drec = new name{"eq", "drec"}; g_eq_mp = new name{"eq", "mp"}; g_eq_mpr = new name{"eq", "mpr"}; g_eq_nrec = new name{"eq", "nrec"}; + g_eq_rec = new name{"eq", "rec"}; g_eq_rec_eq = new name{"eq_rec_eq"}; g_eq_refl = new name{"eq", "refl"}; + g_eq_subst = new name{"eq", "subst"}; g_eq_symm = new name{"eq", "symm"}; g_eq_trans = new name{"eq", "trans"}; - g_eq_subst = new name{"eq", "subst"}; g_exists_elim = new name{"exists", "elim"}; g_false = new name{"false"}; - g_false_rec = new name{"false", "rec"}; g_false_of_true_iff_false = new name{"false_of_true_iff_false"}; + g_false_rec = new name{"false", "rec"}; g_field = new name{"field"}; g_funext = new name{"funext"}; - g_has_zero = new name{"has_zero"}; - g_has_one = new name{"has_one"}; - g_has_zero_zero = new name{"has_zero", "zero"}; - g_has_one_one = new name{"has_one", "one"}; g_has_add = new name{"has_add"}; g_has_div = new name{"has_div"}; g_has_mul = new name{"has_mul"}; g_has_neg = new name{"has_neg"}; + g_has_one = new name{"has_one"}; + g_has_one_one = new name{"has_one", "one"}; g_has_sub = new name{"has_sub"}; + g_has_zero = new name{"has_zero"}; + g_has_zero_zero = new name{"has_zero", "zero"}; g_heq = new name{"heq"}; g_heq_refl = new name{"heq", "refl"}; g_heq_to_eq = new name{"heq", "to_eq"}; g_iff = new name{"iff"}; - g_iff_refl = new name{"iff", "refl"}; - g_iff_symm = new name{"iff", "symm"}; - g_iff_trans = new name{"iff", "trans"}; - g_iff_mp = new name{"iff", "mp"}; - g_iff_mpr = new name{"iff", "mpr"}; - g_iff_intro = new name{"iff", "intro"}; g_iff_elim_left = new name{"iff", "elim_left"}; g_iff_elim_right = new name{"iff", "elim_right"}; g_iff_false_intro = new name{"iff_false_intro"}; + g_iff_intro = new name{"iff", "intro"}; + g_iff_mp = new name{"iff", "mp"}; + g_iff_mpr = new name{"iff", "mpr"}; + g_iff_refl = new name{"iff", "refl"}; + g_iff_symm = new name{"iff", "symm"}; + g_iff_trans = new name{"iff", "trans"}; g_iff_true_intro = new name{"iff_true_intro"}; - g_implies_resolve = new name{"implies", "resolve"}; g_implies = new name{"implies"}; - g_implies_of_if_pos = new name{"implies_of_if_pos"}; g_implies_of_if_neg = new name{"implies_of_if_neg"}; + g_implies_of_if_pos = new name{"implies_of_if_pos"}; + g_implies_resolve = new name{"implies", "resolve"}; + g_is_trunc_is_hprop = new name{"is_trunc", "is_hprop"}; g_is_trunc_is_hprop_elim = new name{"is_trunc", "is_hprop", "elim"}; + g_is_trunc_is_hset = new name{"is_trunc", "is_hset"}; g_ite = new name{"ite"}; - g_le_refl = new name{"le", "refl"}; g_left_distrib = new name{"left_distrib"}; - g_linear_ordered_semiring = new name{"linear_ordered_semiring"}; - g_linear_ordered_ring = new name{"linear_ordered_ring"}; + g_le_refl = new name{"le", "refl"}; g_lift = new name{"lift"}; g_lift_down = new name{"lift", "down"}; g_lift_up = new name{"lift", "up"}; + g_linear_ordered_ring = new name{"linear_ordered_ring"}; + g_linear_ordered_semiring = new name{"linear_ordered_semiring"}; g_monoid = new name{"monoid"}; g_mul = new name{"mul"}; g_mul_one = new name{"mul_one"}; - g_mul_zero_class = new name{"mul_zero_class"}; g_mul_zero = new name{"mul_zero"}; + g_mul_zero_class = new name{"mul_zero_class"}; g_nat = new name{"nat"}; g_nat_of_num = new name{"nat", "of_num"}; g_nat_succ = new name{"nat", "succ"}; g_nat_zero = new name{"nat", "zero"}; g_ne = new name{"ne"}; g_neg = new name{"neg"}; - g_not = new name{"not"}; - g_not_of_iff_false = new name{"not_of_iff_false"}; - g_not_of_not_not_not = new name{"not_of_not_not_not"}; 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_zero = new name{"norm_num", "add1_zero"}; 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_bit1_add_bit0_helper = new name{"norm_num", "bit1_add_bit0_helper"}; g_norm_num_bit0_add_bit1_helper = new name{"norm_num", "bit0_add_bit1_helper"}; - g_norm_num_bit1_add_bit1_helper = new name{"norm_num", "bit1_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_one_add_bit1_helper = new name{"norm_num", "one_add_bit1_helper"}; - g_norm_num_one_add_bit0 = new name{"norm_num", "one_add_bit0"}; - g_norm_num_one_add_one = new name{"norm_num", "one_add_one"}; - g_norm_num_subst_into_prod = new name{"norm_num", "subst_into_prod"}; - g_norm_num_subst_into_sum = new name{"norm_num", "subst_into_sum"}; - g_norm_num_subst_into_subtr = new name{"norm_num", "subst_into_subtr"}; + 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_pos_add_neg_helper = new name{"norm_num", "pos_add_neg_helper"}; 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_pos_mul_neg_helper = new name{"norm_num", "pos_mul_neg_helper"}; - g_norm_num_sub_eq_add_neg_helper = new name{"norm_num", "sub_eq_add_neg_helper"}; - g_norm_num_pos_add_pos_helper = new name{"norm_num", "pos_add_pos_helper"}; g_norm_num_neg_neg_helper = new name{"norm_num", "neg_neg_helper"}; - g_norm_num_add_div_helper = new name{"norm_num", "add_div_helper"}; - g_norm_num_div_add_helper = new name{"norm_num", "div_add_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_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_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_mul_div_helper = new name{"norm_num", "mul_div_helper"}; - g_norm_num_div_mul_helper = new name{"norm_num", "div_mul_helper"}; - g_norm_num_div_helper = new name{"norm_num", "div_helper"}; - g_norm_num_div_eq_div_helper = new name{"norm_num", "div_eq_div_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_add_pos_helper = new name{"norm_num", "pos_add_pos_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_eq_add_neg_helper = new name{"norm_num", "sub_eq_add_neg_helper"}; g_norm_num_subst_into_div = new name{"norm_num", "subst_into_div"}; - g_norm_num_nonzero_of_div_helper = new name{"norm_num", "nonzero_of_div_helper"}; - g_norm_num_neg_zero_helper = new name{"norm_num", "neg_zero_helper"}; + 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_not_not_not = new name{"not_of_not_not_not"}; g_num = new name{"num"}; - g_num_zero = new name{"num", "zero"}; g_num_pos = new name{"num", "pos"}; + g_num_zero = new name{"num", "zero"}; g_of_iff_true = new name{"of_iff_true"}; g_one = new name{"one"}; g_one_mul = new name{"one_mul"}; g_option = new name{"option"}; - g_option_some = new name{"option", "some"}; g_option_none = new name{"option", "none"}; + g_option_some = new name{"option", "some"}; g_or = new name{"or"}; g_or_elim = new name{"or", "elim"}; g_or_intro_left = new name{"or", "intro_left"}; g_or_intro_right = new name{"or", "intro_right"}; + g_or_neg_resolve_left = new name{"or", "neg_resolve_left"}; + g_or_neg_resolve_right = new name{"or", "neg_resolve_right"}; g_or_rec = new name{"or", "rec"}; g_or_resolve_left = new name{"or", "resolve_left"}; g_or_resolve_right = new name{"or", "resolve_right"}; - g_or_neg_resolve_left = new name{"or", "neg_resolve_left"}; - g_or_neg_resolve_right = new name{"or", "neg_resolve_right"}; g_poly_unit = new name{"poly_unit"}; g_poly_unit_star = new name{"poly_unit", "star"}; g_pos_num = new name{"pos_num"}; - g_pos_num_one = new name{"pos_num", "one"}; g_pos_num_bit0 = new name{"pos_num", "bit0"}; g_pos_num_bit1 = new name{"pos_num", "bit1"}; + g_pos_num_one = new name{"pos_num", "one"}; g_prod = new name{"prod"}; g_prod_mk = new name{"prod", "mk"}; g_prod_pr1 = new name{"prod", "pr1"}; @@ -436,8 +438,8 @@ void initialize_constants() { g_propext = new name{"propext"}; g_rat_divide = new name{"rat", "divide"}; g_rat_of_num = new name{"rat", "of_num"}; - g_ring = new name{"ring"}; g_right_distrib = new name{"right_distrib"}; + g_ring = new name{"ring"}; g_semiring = new name{"semiring"}; g_sigma = new name{"sigma"}; g_sigma_mk = new name{"sigma", "mk"}; @@ -450,13 +452,10 @@ void initialize_constants() { g_subsingleton_elim = new name{"subsingleton", "elim"}; g_tactic = new name{"tactic"}; g_tactic_all_goals = new name{"tactic", "all_goals"}; - g_tactic_apply = new name{"tactic", "apply"}; - g_tactic_assert_hypothesis = new name{"tactic", "assert_hypothesis"}; - g_tactic_eapply = new name{"tactic", "eapply"}; - g_tactic_fapply = new name{"tactic", "fapply"}; - g_tactic_eassumption = new name{"tactic", "eassumption"}; g_tactic_and_then = new name{"tactic", "and_then"}; g_tactic_append = new name{"tactic", "append"}; + g_tactic_apply = new name{"tactic", "apply"}; + g_tactic_assert_hypothesis = new name{"tactic", "assert_hypothesis"}; g_tactic_assumption = new name{"tactic", "assumption"}; g_tactic_at_most = new name{"tactic", "at_most"}; g_tactic_beta = new name{"tactic", "beta"}; @@ -468,30 +467,32 @@ void initialize_constants() { g_tactic_clears = new name{"tactic", "clears"}; g_tactic_determ = new name{"tactic", "determ"}; g_tactic_discard = new name{"tactic", "discard"}; - g_tactic_intro = new name{"tactic", "intro"}; - g_tactic_intros = new name{"tactic", "intros"}; + g_tactic_eapply = new name{"tactic", "eapply"}; + g_tactic_eassumption = new name{"tactic", "eassumption"}; g_tactic_exact = new name{"tactic", "exact"}; g_tactic_expr = new name{"tactic", "expr"}; g_tactic_expr_builtin = new name{"tactic", "expr", "builtin"}; g_tactic_expr_list = new name{"tactic", "expr_list"}; g_tactic_expr_list_cons = new name{"tactic", "expr_list", "cons"}; g_tactic_expr_list_nil = new name{"tactic", "expr_list", "nil"}; - g_tactic_using_expr = new name{"tactic", "using_expr"}; - g_tactic_none_expr = new name{"tactic", "none_expr"}; - g_tactic_identifier = new name{"tactic", "identifier"}; - g_tactic_identifier_list = new name{"tactic", "identifier_list"}; - g_tactic_opt_expr = new name{"tactic", "opt_expr"}; - g_tactic_opt_identifier_list = new name{"tactic", "opt_identifier_list"}; g_tactic_fail = new name{"tactic", "fail"}; + g_tactic_fapply = new name{"tactic", "fapply"}; g_tactic_fixpoint = new name{"tactic", "fixpoint"}; g_tactic_focus_at = new name{"tactic", "focus_at"}; - g_tactic_generalize_tac = new name{"tactic", "generalize_tac"}; g_tactic_generalizes = new name{"tactic", "generalizes"}; + g_tactic_generalize_tac = new name{"tactic", "generalize_tac"}; g_tactic_id = new name{"tactic", "id"}; + g_tactic_identifier = new name{"tactic", "identifier"}; + g_tactic_identifier_list = new name{"tactic", "identifier_list"}; g_tactic_interleave = new name{"tactic", "interleave"}; + g_tactic_intro = new name{"tactic", "intro"}; + g_tactic_intros = new name{"tactic", "intros"}; g_tactic_lettac = new name{"tactic", "lettac"}; + g_tactic_none_expr = new name{"tactic", "none_expr"}; g_tactic_now = new name{"tactic", "now"}; + g_tactic_opt_expr = new name{"tactic", "opt_expr"}; g_tactic_opt_expr_list = new name{"tactic", "opt_expr_list"}; + g_tactic_opt_identifier_list = new name{"tactic", "opt_identifier_list"}; g_tactic_or_else = new name{"tactic", "or_else"}; g_tactic_par = new name{"tactic", "par"}; g_tactic_refine = new name{"tactic", "refine"}; @@ -505,27 +506,26 @@ void initialize_constants() { g_tactic_state = new name{"tactic", "state"}; g_tactic_trace = new name{"tactic", "trace"}; g_tactic_try_for = new name{"tactic", "try_for"}; + g_tactic_using_expr = new name{"tactic", "using_expr"}; g_tactic_whnf = new name{"tactic", "whnf"}; 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_is_trunc_is_hset = new name{"is_trunc", "is_hset"}; - g_is_trunc_is_hprop = new name{"is_trunc", "is_hprop"}; g_weak_order = new name{"weak_order"}; g_well_founded = new name{"well_founded"}; g_zero = new name{"zero"}; - g_zero_mul = new name{"zero_mul"}; 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_add; delete g_add_comm_group; delete g_add_comm_semigroup; - delete g_add_monoid; delete g_add_group; + delete g_add_monoid; delete g_and; delete g_and_elim_left; delete g_and_elim_right; @@ -549,145 +549,147 @@ void finalize_constants() { delete g_empty; delete g_empty_rec; delete g_eq; + delete g_eq_drec; delete g_eq_elim_inv_inv; delete g_eq_intro; - delete g_eq_rec; - delete g_eq_drec; delete g_eq_mp; delete g_eq_mpr; delete g_eq_nrec; + delete g_eq_rec; delete g_eq_rec_eq; delete g_eq_refl; + delete g_eq_subst; delete g_eq_symm; delete g_eq_trans; - delete g_eq_subst; delete g_exists_elim; delete g_false; - delete g_false_rec; delete g_false_of_true_iff_false; + delete g_false_rec; delete g_field; delete g_funext; - delete g_has_zero; - delete g_has_one; - delete g_has_zero_zero; - delete g_has_one_one; delete g_has_add; delete g_has_div; delete g_has_mul; delete g_has_neg; + delete g_has_one; + delete g_has_one_one; delete g_has_sub; + delete g_has_zero; + delete g_has_zero_zero; delete g_heq; delete g_heq_refl; delete g_heq_to_eq; delete g_iff; - delete g_iff_refl; - delete g_iff_symm; - delete g_iff_trans; - delete g_iff_mp; - delete g_iff_mpr; - delete g_iff_intro; delete g_iff_elim_left; delete g_iff_elim_right; delete g_iff_false_intro; + delete g_iff_intro; + 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_implies_resolve; delete g_implies; - delete g_implies_of_if_pos; delete g_implies_of_if_neg; + delete g_implies_of_if_pos; + delete g_implies_resolve; + delete g_is_trunc_is_hprop; delete g_is_trunc_is_hprop_elim; + delete g_is_trunc_is_hset; delete g_ite; - delete g_le_refl; delete g_left_distrib; - delete g_linear_ordered_semiring; - delete g_linear_ordered_ring; + delete g_le_refl; delete g_lift; delete g_lift_down; delete g_lift_up; + delete g_linear_ordered_ring; + delete g_linear_ordered_semiring; delete g_monoid; delete g_mul; delete g_mul_one; - delete g_mul_zero_class; delete g_mul_zero; + delete g_mul_zero_class; delete g_nat; delete g_nat_of_num; delete g_nat_succ; delete g_nat_zero; delete g_ne; delete g_neg; - delete g_not; - delete g_not_of_iff_false; - delete g_not_of_not_not_not; delete g_norm_num_add1; delete g_norm_num_add1_bit0; delete g_norm_num_add1_bit1_helper; - delete g_norm_num_add1_zero; 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_bit1_add_bit0_helper; delete g_norm_num_bit0_add_bit1_helper; - delete g_norm_num_bit1_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_one_add_bit1_helper; - delete g_norm_num_one_add_bit0; - delete g_norm_num_one_add_one; - delete g_norm_num_subst_into_prod; - delete g_norm_num_subst_into_sum; - delete g_norm_num_subst_into_subtr; + 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_pos_add_neg_helper; delete g_norm_num_neg_mul_neg_helper; delete g_norm_num_neg_mul_pos_helper; - delete g_norm_num_pos_mul_neg_helper; - delete g_norm_num_sub_eq_add_neg_helper; - delete g_norm_num_pos_add_pos_helper; delete g_norm_num_neg_neg_helper; - delete g_norm_num_add_div_helper; - delete g_norm_num_div_add_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_pos_bit0_helper; - delete g_norm_num_pos_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_mul_div_helper; - delete g_norm_num_div_mul_helper; - delete g_norm_num_div_helper; - delete g_norm_num_div_eq_div_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_add_pos_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_eq_add_neg_helper; delete g_norm_num_subst_into_div; - delete g_norm_num_nonzero_of_div_helper; - delete g_norm_num_neg_zero_helper; + 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_not_not_not; delete g_num; - delete g_num_zero; delete g_num_pos; + delete g_num_zero; delete g_of_iff_true; delete g_one; delete g_one_mul; delete g_option; - delete g_option_some; delete g_option_none; + delete g_option_some; delete g_or; delete g_or_elim; delete g_or_intro_left; delete g_or_intro_right; + delete g_or_neg_resolve_left; + delete g_or_neg_resolve_right; delete g_or_rec; delete g_or_resolve_left; delete g_or_resolve_right; - delete g_or_neg_resolve_left; - delete g_or_neg_resolve_right; delete g_poly_unit; delete g_poly_unit_star; delete g_pos_num; - delete g_pos_num_one; delete g_pos_num_bit0; delete g_pos_num_bit1; + delete g_pos_num_one; delete g_prod; delete g_prod_mk; delete g_prod_pr1; @@ -695,8 +697,8 @@ void finalize_constants() { delete g_propext; delete g_rat_divide; delete g_rat_of_num; - delete g_ring; delete g_right_distrib; + delete g_ring; delete g_semiring; delete g_sigma; delete g_sigma_mk; @@ -709,13 +711,10 @@ void finalize_constants() { delete g_subsingleton_elim; delete g_tactic; delete g_tactic_all_goals; - delete g_tactic_apply; - delete g_tactic_assert_hypothesis; - delete g_tactic_eapply; - delete g_tactic_fapply; - delete g_tactic_eassumption; delete g_tactic_and_then; delete g_tactic_append; + delete g_tactic_apply; + delete g_tactic_assert_hypothesis; delete g_tactic_assumption; delete g_tactic_at_most; delete g_tactic_beta; @@ -727,30 +726,32 @@ void finalize_constants() { delete g_tactic_clears; delete g_tactic_determ; delete g_tactic_discard; - delete g_tactic_intro; - delete g_tactic_intros; + delete g_tactic_eapply; + delete g_tactic_eassumption; delete g_tactic_exact; delete g_tactic_expr; delete g_tactic_expr_builtin; delete g_tactic_expr_list; delete g_tactic_expr_list_cons; delete g_tactic_expr_list_nil; - delete g_tactic_using_expr; - delete g_tactic_none_expr; - delete g_tactic_identifier; - delete g_tactic_identifier_list; - delete g_tactic_opt_expr; - delete g_tactic_opt_identifier_list; delete g_tactic_fail; + delete g_tactic_fapply; delete g_tactic_fixpoint; delete g_tactic_focus_at; - delete g_tactic_generalize_tac; delete g_tactic_generalizes; + delete g_tactic_generalize_tac; delete g_tactic_id; + delete g_tactic_identifier; + delete g_tactic_identifier_list; delete g_tactic_interleave; + delete g_tactic_intro; + delete g_tactic_intros; delete g_tactic_lettac; + delete g_tactic_none_expr; delete g_tactic_now; + delete g_tactic_opt_expr; delete g_tactic_opt_expr_list; + delete g_tactic_opt_identifier_list; delete g_tactic_or_else; delete g_tactic_par; delete g_tactic_refine; @@ -764,26 +765,25 @@ void finalize_constants() { delete g_tactic_state; delete g_tactic_trace; delete g_tactic_try_for; + delete g_tactic_using_expr; delete g_tactic_whnf; delete g_trans_rel_left; delete g_trans_rel_right; delete g_true; delete g_true_intro; - delete g_is_trunc_is_hset; - delete g_is_trunc_is_hprop; delete g_weak_order; delete g_well_founded; delete g_zero; - delete g_zero_mul; 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_add_name() { return *g_add; } 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_monoid_name() { return *g_add_monoid; } 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; } @@ -807,145 +807,147 @@ name const & get_div_name() { return *g_div; } name const & get_empty_name() { return *g_empty; } name const & get_empty_rec_name() { return *g_empty_rec; } name const & get_eq_name() { return *g_eq; } +name const & get_eq_drec_name() { return *g_eq_drec; } name const & get_eq_elim_inv_inv_name() { return *g_eq_elim_inv_inv; } name const & get_eq_intro_name() { return *g_eq_intro; } -name const & get_eq_rec_name() { return *g_eq_rec; } -name const & get_eq_drec_name() { return *g_eq_drec; } name const & get_eq_mp_name() { return *g_eq_mp; } name const & get_eq_mpr_name() { return *g_eq_mpr; } name const & get_eq_nrec_name() { return *g_eq_nrec; } +name const & get_eq_rec_name() { return *g_eq_rec; } name const & get_eq_rec_eq_name() { return *g_eq_rec_eq; } 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_subst_name() { return *g_eq_subst; } name const & get_exists_elim_name() { return *g_exists_elim; } name const & get_false_name() { return *g_false; } -name const & get_false_rec_name() { return *g_false_rec; } name const & get_false_of_true_iff_false_name() { return *g_false_of_true_iff_false; } +name const & get_false_rec_name() { return *g_false_rec; } name const & get_field_name() { return *g_field; } name const & get_funext_name() { return *g_funext; } -name const & get_has_zero_name() { return *g_has_zero; } -name const & get_has_one_name() { return *g_has_one; } -name const & get_has_zero_zero_name() { return *g_has_zero_zero; } -name const & get_has_one_one_name() { return *g_has_one_one; } name const & get_has_add_name() { return *g_has_add; } name const & get_has_div_name() { return *g_has_div; } name const & get_has_mul_name() { return *g_has_mul; } name const & get_has_neg_name() { return *g_has_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_sub_name() { return *g_has_sub; } +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_heq_name() { return *g_heq; } name const & get_heq_refl_name() { return *g_heq_refl; } name const & get_heq_to_eq_name() { return *g_heq_to_eq; } name const & get_iff_name() { return *g_iff; } -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_mp_name() { return *g_iff_mp; } -name const & get_iff_mpr_name() { return *g_iff_mpr; } -name const & get_iff_intro_name() { return *g_iff_intro; } name const & get_iff_elim_left_name() { return *g_iff_elim_left; } name const & get_iff_elim_right_name() { return *g_iff_elim_right; } name const & get_iff_false_intro_name() { return *g_iff_false_intro; } +name const & get_iff_intro_name() { return *g_iff_intro; } +name const & get_iff_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_implies_resolve_name() { return *g_implies_resolve; } name const & get_implies_name() { return *g_implies; } -name const & get_implies_of_if_pos_name() { return *g_implies_of_if_pos; } 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_implies_resolve_name() { return *g_implies_resolve; } +name const & get_is_trunc_is_hprop_name() { return *g_is_trunc_is_hprop; } name const & get_is_trunc_is_hprop_elim_name() { return *g_is_trunc_is_hprop_elim; } +name const & get_is_trunc_is_hset_name() { return *g_is_trunc_is_hset; } name const & get_ite_name() { return *g_ite; } -name const & get_le_refl_name() { return *g_le_refl; } name const & get_left_distrib_name() { return *g_left_distrib; } -name const & get_linear_ordered_semiring_name() { return *g_linear_ordered_semiring; } -name const & get_linear_ordered_ring_name() { return *g_linear_ordered_ring; } +name const & get_le_refl_name() { return *g_le_refl; } name const & get_lift_name() { return *g_lift; } name const & get_lift_down_name() { return *g_lift_down; } name const & get_lift_up_name() { return *g_lift_up; } +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_monoid_name() { return *g_monoid; } name const & get_mul_name() { return *g_mul; } name const & get_mul_one_name() { return *g_mul_one; } -name const & get_mul_zero_class_name() { return *g_mul_zero_class; } 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_nat_name() { return *g_nat; } name const & get_nat_of_num_name() { return *g_nat_of_num; } name const & get_nat_succ_name() { return *g_nat_succ; } name const & get_nat_zero_name() { return *g_nat_zero; } name const & get_ne_name() { return *g_ne; } name const & get_neg_name() { return *g_neg; } -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_not_not_not_name() { return *g_not_of_not_not_not; } 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_zero_name() { return *g_norm_num_add1_zero; } 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_bit1_add_bit0_helper_name() { return *g_norm_num_bit1_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_bit1_add_bit1_helper_name() { return *g_norm_num_bit1_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_one_add_bit1_helper_name() { return *g_norm_num_one_add_bit1_helper; } -name const & get_norm_num_one_add_bit0_name() { return *g_norm_num_one_add_bit0; } -name const & get_norm_num_one_add_one_name() { return *g_norm_num_one_add_one; } -name const & get_norm_num_subst_into_prod_name() { return *g_norm_num_subst_into_prod; } -name const & get_norm_num_subst_into_sum_name() { return *g_norm_num_subst_into_sum; } -name const & get_norm_num_subst_into_subtr_name() { return *g_norm_num_subst_into_subtr; } +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_pos_add_neg_helper_name() { return *g_norm_num_pos_add_neg_helper; } 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_pos_mul_neg_helper_name() { return *g_norm_num_pos_mul_neg_helper; } -name const & get_norm_num_sub_eq_add_neg_helper_name() { return *g_norm_num_sub_eq_add_neg_helper; } -name const & get_norm_num_pos_add_pos_helper_name() { return *g_norm_num_pos_add_pos_helper; } name const & get_norm_num_neg_neg_helper_name() { return *g_norm_num_neg_neg_helper; } -name const & get_norm_num_add_div_helper_name() { return *g_norm_num_add_div_helper; } -name const & get_norm_num_div_add_helper_name() { return *g_norm_num_div_add_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_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_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_mul_div_helper_name() { return *g_norm_num_mul_div_helper; } -name const & get_norm_num_div_mul_helper_name() { return *g_norm_num_div_mul_helper; } -name const & get_norm_num_div_helper_name() { return *g_norm_num_div_helper; } -name const & get_norm_num_div_eq_div_helper_name() { return *g_norm_num_div_eq_div_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_add_pos_helper_name() { return *g_norm_num_pos_add_pos_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_eq_add_neg_helper_name() { return *g_norm_num_sub_eq_add_neg_helper; } name const & get_norm_num_subst_into_div_name() { return *g_norm_num_subst_into_div; } -name const & get_norm_num_nonzero_of_div_helper_name() { return *g_norm_num_nonzero_of_div_helper; } -name const & get_norm_num_neg_zero_helper_name() { return *g_norm_num_neg_zero_helper; } +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_not_not_not_name() { return *g_not_of_not_not_not; } name const & get_num_name() { return *g_num; } -name const & get_num_zero_name() { return *g_num_zero; } name const & get_num_pos_name() { return *g_num_pos; } +name const & get_num_zero_name() { return *g_num_zero; } name const & get_of_iff_true_name() { return *g_of_iff_true; } name const & get_one_name() { return *g_one; } name const & get_one_mul_name() { return *g_one_mul; } name const & get_option_name() { return *g_option; } -name const & get_option_some_name() { return *g_option_some; } name const & get_option_none_name() { return *g_option_none; } +name const & get_option_some_name() { return *g_option_some; } name const & get_or_name() { return *g_or; } name const & get_or_elim_name() { return *g_or_elim; } name const & get_or_intro_left_name() { return *g_or_intro_left; } name const & get_or_intro_right_name() { return *g_or_intro_right; } +name const & get_or_neg_resolve_left_name() { return *g_or_neg_resolve_left; } +name const & get_or_neg_resolve_right_name() { return *g_or_neg_resolve_right; } name const & get_or_rec_name() { return *g_or_rec; } name const & get_or_resolve_left_name() { return *g_or_resolve_left; } name const & get_or_resolve_right_name() { return *g_or_resolve_right; } -name const & get_or_neg_resolve_left_name() { return *g_or_neg_resolve_left; } -name const & get_or_neg_resolve_right_name() { return *g_or_neg_resolve_right; } name const & get_poly_unit_name() { return *g_poly_unit; } name const & get_poly_unit_star_name() { return *g_poly_unit_star; } name const & get_pos_num_name() { return *g_pos_num; } -name const & get_pos_num_one_name() { return *g_pos_num_one; } name const & get_pos_num_bit0_name() { return *g_pos_num_bit0; } name const & get_pos_num_bit1_name() { return *g_pos_num_bit1; } +name const & get_pos_num_one_name() { return *g_pos_num_one; } name const & get_prod_name() { return *g_prod; } name const & get_prod_mk_name() { return *g_prod_mk; } name const & get_prod_pr1_name() { return *g_prod_pr1; } @@ -953,8 +955,8 @@ name const & get_prod_pr2_name() { return *g_prod_pr2; } name const & get_propext_name() { return *g_propext; } name const & get_rat_divide_name() { return *g_rat_divide; } name const & get_rat_of_num_name() { return *g_rat_of_num; } -name const & get_ring_name() { return *g_ring; } name const & get_right_distrib_name() { return *g_right_distrib; } +name const & get_ring_name() { return *g_ring; } name const & get_semiring_name() { return *g_semiring; } name const & get_sigma_name() { return *g_sigma; } name const & get_sigma_mk_name() { return *g_sigma_mk; } @@ -967,13 +969,10 @@ name const & get_subsingleton_name() { return *g_subsingleton; } name const & get_subsingleton_elim_name() { return *g_subsingleton_elim; } name const & get_tactic_name() { return *g_tactic; } name const & get_tactic_all_goals_name() { return *g_tactic_all_goals; } -name const & get_tactic_apply_name() { return *g_tactic_apply; } -name const & get_tactic_assert_hypothesis_name() { return *g_tactic_assert_hypothesis; } -name const & get_tactic_eapply_name() { return *g_tactic_eapply; } -name const & get_tactic_fapply_name() { return *g_tactic_fapply; } -name const & get_tactic_eassumption_name() { return *g_tactic_eassumption; } name const & get_tactic_and_then_name() { return *g_tactic_and_then; } name const & get_tactic_append_name() { return *g_tactic_append; } +name const & get_tactic_apply_name() { return *g_tactic_apply; } +name const & get_tactic_assert_hypothesis_name() { return *g_tactic_assert_hypothesis; } name const & get_tactic_assumption_name() { return *g_tactic_assumption; } name const & get_tactic_at_most_name() { return *g_tactic_at_most; } name const & get_tactic_beta_name() { return *g_tactic_beta; } @@ -985,30 +984,32 @@ name const & get_tactic_clear_name() { return *g_tactic_clear; } name const & get_tactic_clears_name() { return *g_tactic_clears; } name const & get_tactic_determ_name() { return *g_tactic_determ; } name const & get_tactic_discard_name() { return *g_tactic_discard; } -name const & get_tactic_intro_name() { return *g_tactic_intro; } -name const & get_tactic_intros_name() { return *g_tactic_intros; } +name const & get_tactic_eapply_name() { return *g_tactic_eapply; } +name const & get_tactic_eassumption_name() { return *g_tactic_eassumption; } name const & get_tactic_exact_name() { return *g_tactic_exact; } name const & get_tactic_expr_name() { return *g_tactic_expr; } name const & get_tactic_expr_builtin_name() { return *g_tactic_expr_builtin; } name const & get_tactic_expr_list_name() { return *g_tactic_expr_list; } name const & get_tactic_expr_list_cons_name() { return *g_tactic_expr_list_cons; } name const & get_tactic_expr_list_nil_name() { return *g_tactic_expr_list_nil; } -name const & get_tactic_using_expr_name() { return *g_tactic_using_expr; } -name const & get_tactic_none_expr_name() { return *g_tactic_none_expr; } -name const & get_tactic_identifier_name() { return *g_tactic_identifier; } -name const & get_tactic_identifier_list_name() { return *g_tactic_identifier_list; } -name const & get_tactic_opt_expr_name() { return *g_tactic_opt_expr; } -name const & get_tactic_opt_identifier_list_name() { return *g_tactic_opt_identifier_list; } name const & get_tactic_fail_name() { return *g_tactic_fail; } +name const & get_tactic_fapply_name() { return *g_tactic_fapply; } name const & get_tactic_fixpoint_name() { return *g_tactic_fixpoint; } name const & get_tactic_focus_at_name() { return *g_tactic_focus_at; } -name const & get_tactic_generalize_tac_name() { return *g_tactic_generalize_tac; } name const & get_tactic_generalizes_name() { return *g_tactic_generalizes; } +name const & get_tactic_generalize_tac_name() { return *g_tactic_generalize_tac; } name const & get_tactic_id_name() { return *g_tactic_id; } +name const & get_tactic_identifier_name() { return *g_tactic_identifier; } +name const & get_tactic_identifier_list_name() { return *g_tactic_identifier_list; } name const & get_tactic_interleave_name() { return *g_tactic_interleave; } +name const & get_tactic_intro_name() { return *g_tactic_intro; } +name const & get_tactic_intros_name() { return *g_tactic_intros; } name const & get_tactic_lettac_name() { return *g_tactic_lettac; } +name const & get_tactic_none_expr_name() { return *g_tactic_none_expr; } name const & get_tactic_now_name() { return *g_tactic_now; } +name const & get_tactic_opt_expr_name() { return *g_tactic_opt_expr; } name const & get_tactic_opt_expr_list_name() { return *g_tactic_opt_expr_list; } +name const & get_tactic_opt_identifier_list_name() { return *g_tactic_opt_identifier_list; } name const & get_tactic_or_else_name() { return *g_tactic_or_else; } name const & get_tactic_par_name() { return *g_tactic_par; } name const & get_tactic_refine_name() { return *g_tactic_refine; } @@ -1022,17 +1023,16 @@ name const & get_tactic_rotate_right_name() { return *g_tactic_rotate_right; } name const & get_tactic_state_name() { return *g_tactic_state; } name const & get_tactic_trace_name() { return *g_tactic_trace; } name const & get_tactic_try_for_name() { return *g_tactic_try_for; } +name const & get_tactic_using_expr_name() { return *g_tactic_using_expr; } name const & get_tactic_whnf_name() { return *g_tactic_whnf; } 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_is_trunc_is_hset_name() { return *g_is_trunc_is_hset; } -name const & get_is_trunc_is_hprop_name() { return *g_is_trunc_is_hprop; } name const & get_weak_order_name() { return *g_weak_order; } name const & get_well_founded_name() { return *g_well_founded; } name const & get_zero_name() { return *g_zero; } -name const & get_zero_mul_name() { return *g_zero_mul; } name const & get_zero_le_one_name() { return *g_zero_le_one; } name const & get_zero_lt_one_name() { return *g_zero_lt_one; } +name const & get_zero_mul_name() { return *g_zero_mul; } } diff --git a/src/library/constants.h b/src/library/constants.h index a3e77fa7b..26ba43162 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -9,8 +9,8 @@ name const & get_absurd_name(); name const & get_add_name(); name const & get_add_comm_group_name(); name const & get_add_comm_semigroup_name(); -name const & get_add_monoid_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(); @@ -34,145 +34,147 @@ name const & get_div_name(); name const & get_empty_name(); name const & get_empty_rec_name(); name const & get_eq_name(); +name const & get_eq_drec_name(); name const & get_eq_elim_inv_inv_name(); name const & get_eq_intro_name(); -name const & get_eq_rec_name(); -name const & get_eq_drec_name(); name const & get_eq_mp_name(); name const & get_eq_mpr_name(); name const & get_eq_nrec_name(); +name const & get_eq_rec_name(); name const & get_eq_rec_eq_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_subst_name(); name const & get_exists_elim_name(); name const & get_false_name(); -name const & get_false_rec_name(); name const & get_false_of_true_iff_false_name(); +name const & get_false_rec_name(); name const & get_field_name(); name const & get_funext_name(); -name const & get_has_zero_name(); -name const & get_has_one_name(); -name const & get_has_zero_zero_name(); -name const & get_has_one_one_name(); name const & get_has_add_name(); name const & get_has_div_name(); name const & get_has_mul_name(); name const & get_has_neg_name(); +name const & get_has_one_name(); +name const & get_has_one_one_name(); name const & get_has_sub_name(); +name const & get_has_zero_name(); +name const & get_has_zero_zero_name(); name const & get_heq_name(); name const & get_heq_refl_name(); name const & get_heq_to_eq_name(); name const & get_iff_name(); -name const & get_iff_refl_name(); -name const & get_iff_symm_name(); -name const & get_iff_trans_name(); -name const & get_iff_mp_name(); -name const & get_iff_mpr_name(); -name const & get_iff_intro_name(); name const & get_iff_elim_left_name(); name const & get_iff_elim_right_name(); name const & get_iff_false_intro_name(); +name const & get_iff_intro_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_implies_resolve_name(); name const & get_implies_name(); -name const & get_implies_of_if_pos_name(); name const & get_implies_of_if_neg_name(); +name const & get_implies_of_if_pos_name(); +name const & get_implies_resolve_name(); +name const & get_is_trunc_is_hprop_name(); name const & get_is_trunc_is_hprop_elim_name(); +name const & get_is_trunc_is_hset_name(); name const & get_ite_name(); -name const & get_le_refl_name(); name const & get_left_distrib_name(); -name const & get_linear_ordered_semiring_name(); -name const & get_linear_ordered_ring_name(); +name const & get_le_refl_name(); name const & get_lift_name(); name const & get_lift_down_name(); name const & get_lift_up_name(); +name const & get_linear_ordered_ring_name(); +name const & get_linear_ordered_semiring_name(); name const & get_monoid_name(); name const & get_mul_name(); name const & get_mul_one_name(); -name const & get_mul_zero_class_name(); name const & get_mul_zero_name(); +name const & get_mul_zero_class_name(); name const & get_nat_name(); name const & get_nat_of_num_name(); name const & get_nat_succ_name(); name const & get_nat_zero_name(); name const & get_ne_name(); name const & get_neg_name(); -name const & get_not_name(); -name const & get_not_of_iff_false_name(); -name const & get_not_of_not_not_not_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_zero_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_bit1_add_bit0_helper_name(); name const & get_norm_num_bit0_add_bit1_helper_name(); -name const & get_norm_num_bit1_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_one_add_bit1_helper_name(); -name const & get_norm_num_one_add_bit0_name(); -name const & get_norm_num_one_add_one_name(); -name const & get_norm_num_subst_into_prod_name(); -name const & get_norm_num_subst_into_sum_name(); -name const & get_norm_num_subst_into_subtr_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_pos_add_neg_helper_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_pos_mul_neg_helper_name(); -name const & get_norm_num_sub_eq_add_neg_helper_name(); -name const & get_norm_num_pos_add_pos_helper_name(); name const & get_norm_num_neg_neg_helper_name(); -name const & get_norm_num_add_div_helper_name(); -name const & get_norm_num_div_add_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_pos_bit0_helper_name(); -name const & get_norm_num_pos_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_mul_div_helper_name(); -name const & get_norm_num_div_mul_helper_name(); -name const & get_norm_num_div_helper_name(); -name const & get_norm_num_div_eq_div_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_add_pos_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_eq_add_neg_helper_name(); name const & get_norm_num_subst_into_div_name(); -name const & get_norm_num_nonzero_of_div_helper_name(); -name const & get_norm_num_neg_zero_helper_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_not_not_not_name(); name const & get_num_name(); -name const & get_num_zero_name(); name const & get_num_pos_name(); +name const & get_num_zero_name(); name const & get_of_iff_true_name(); name const & get_one_name(); name const & get_one_mul_name(); name const & get_option_name(); -name const & get_option_some_name(); name const & get_option_none_name(); +name const & get_option_some_name(); name const & get_or_name(); name const & get_or_elim_name(); name const & get_or_intro_left_name(); name const & get_or_intro_right_name(); +name const & get_or_neg_resolve_left_name(); +name const & get_or_neg_resolve_right_name(); name const & get_or_rec_name(); name const & get_or_resolve_left_name(); name const & get_or_resolve_right_name(); -name const & get_or_neg_resolve_left_name(); -name const & get_or_neg_resolve_right_name(); name const & get_poly_unit_name(); name const & get_poly_unit_star_name(); name const & get_pos_num_name(); -name const & get_pos_num_one_name(); name const & get_pos_num_bit0_name(); name const & get_pos_num_bit1_name(); +name const & get_pos_num_one_name(); name const & get_prod_name(); name const & get_prod_mk_name(); name const & get_prod_pr1_name(); @@ -180,8 +182,8 @@ name const & get_prod_pr2_name(); name const & get_propext_name(); name const & get_rat_divide_name(); name const & get_rat_of_num_name(); -name const & get_ring_name(); name const & get_right_distrib_name(); +name const & get_ring_name(); name const & get_semiring_name(); name const & get_sigma_name(); name const & get_sigma_mk_name(); @@ -194,13 +196,10 @@ name const & get_subsingleton_name(); name const & get_subsingleton_elim_name(); name const & get_tactic_name(); name const & get_tactic_all_goals_name(); -name const & get_tactic_apply_name(); -name const & get_tactic_assert_hypothesis_name(); -name const & get_tactic_eapply_name(); -name const & get_tactic_fapply_name(); -name const & get_tactic_eassumption_name(); name const & get_tactic_and_then_name(); name const & get_tactic_append_name(); +name const & get_tactic_apply_name(); +name const & get_tactic_assert_hypothesis_name(); name const & get_tactic_assumption_name(); name const & get_tactic_at_most_name(); name const & get_tactic_beta_name(); @@ -212,30 +211,32 @@ name const & get_tactic_clear_name(); name const & get_tactic_clears_name(); name const & get_tactic_determ_name(); name const & get_tactic_discard_name(); -name const & get_tactic_intro_name(); -name const & get_tactic_intros_name(); +name const & get_tactic_eapply_name(); +name const & get_tactic_eassumption_name(); name const & get_tactic_exact_name(); name const & get_tactic_expr_name(); name const & get_tactic_expr_builtin_name(); name const & get_tactic_expr_list_name(); name const & get_tactic_expr_list_cons_name(); name const & get_tactic_expr_list_nil_name(); -name const & get_tactic_using_expr_name(); -name const & get_tactic_none_expr_name(); -name const & get_tactic_identifier_name(); -name const & get_tactic_identifier_list_name(); -name const & get_tactic_opt_expr_name(); -name const & get_tactic_opt_identifier_list_name(); name const & get_tactic_fail_name(); +name const & get_tactic_fapply_name(); name const & get_tactic_fixpoint_name(); name const & get_tactic_focus_at_name(); -name const & get_tactic_generalize_tac_name(); name const & get_tactic_generalizes_name(); +name const & get_tactic_generalize_tac_name(); name const & get_tactic_id_name(); +name const & get_tactic_identifier_name(); +name const & get_tactic_identifier_list_name(); name const & get_tactic_interleave_name(); +name const & get_tactic_intro_name(); +name const & get_tactic_intros_name(); name const & get_tactic_lettac_name(); +name const & get_tactic_none_expr_name(); name const & get_tactic_now_name(); +name const & get_tactic_opt_expr_name(); name const & get_tactic_opt_expr_list_name(); +name const & get_tactic_opt_identifier_list_name(); name const & get_tactic_or_else_name(); name const & get_tactic_par_name(); name const & get_tactic_refine_name(); @@ -249,17 +250,16 @@ name const & get_tactic_rotate_right_name(); name const & get_tactic_state_name(); name const & get_tactic_trace_name(); name const & get_tactic_try_for_name(); +name const & get_tactic_using_expr_name(); name const & get_tactic_whnf_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_is_trunc_is_hset_name(); -name const & get_is_trunc_is_hprop_name(); name const & get_weak_order_name(); name const & get_well_founded_name(); name const & get_zero_name(); -name const & get_zero_mul_name(); name const & get_zero_le_one_name(); name const & get_zero_lt_one_name(); +name const & get_zero_mul_name(); } diff --git a/src/library/constants.txt b/src/library/constants.txt index a8eaf34e2..90621cf04 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -2,8 +2,8 @@ absurd add add_comm_group add_comm_semigroup -add_monoid add_group +add_monoid and and.elim_left and.elim_right @@ -27,145 +27,147 @@ div empty empty.rec eq +eq.drec eq.elim_inv_inv eq.intro -eq.rec -eq.drec eq.mp eq.mpr eq.nrec +eq.rec eq_rec_eq eq.refl +eq.subst eq.symm eq.trans -eq.subst exists.elim false -false.rec false_of_true_iff_false +false.rec field funext -has_zero -has_one -has_zero.zero -has_one.one has_add has_div has_mul has_neg +has_one +has_one.one has_sub +has_zero +has_zero.zero heq heq.refl heq.to_eq iff -iff.refl -iff.symm -iff.trans -iff.mp -iff.mpr -iff.intro iff.elim_left iff.elim_right iff_false_intro +iff.intro +iff.mp +iff.mpr +iff.refl +iff.symm +iff.trans iff_true_intro -implies.resolve implies -implies_of_if_pos implies_of_if_neg +implies_of_if_pos +implies.resolve +is_trunc.is_hprop is_trunc.is_hprop.elim +is_trunc.is_hset ite -le.refl left_distrib -linear_ordered_semiring -linear_ordered_ring +le.refl lift lift.down lift.up +linear_ordered_ring +linear_ordered_semiring monoid mul mul_one -mul_zero_class mul_zero +mul_zero_class nat nat.of_num nat.succ nat.zero ne neg -not -not_of_iff_false -not_of_not_not_not norm_num.add1 norm_num.add1_bit0 norm_num.add1_bit1_helper -norm_num.add1_zero 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.bit1_add_bit0_helper norm_num.bit0_add_bit1_helper -norm_num.bit1_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.one_add_bit1_helper -norm_num.one_add_bit0 -norm_num.one_add_one -norm_num.subst_into_prod -norm_num.subst_into_sum -norm_num.subst_into_subtr +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.pos_add_neg_helper norm_num.neg_mul_neg_helper norm_num.neg_mul_pos_helper -norm_num.pos_mul_neg_helper -norm_num.sub_eq_add_neg_helper -norm_num.pos_add_pos_helper norm_num.neg_neg_helper -norm_num.add_div_helper -norm_num.div_add_helper +norm_num.neg_zero_helper norm_num.nonneg_bit0_helper norm_num.nonneg_bit1_helper -norm_num.pos_bit0_helper -norm_num.pos_bit1_helper +norm_num.nonzero_of_div_helper norm_num.nonzero_of_neg_helper norm_num.nonzero_of_pos_helper -norm_num.mul_div_helper -norm_num.div_mul_helper -norm_num.div_helper -norm_num.div_eq_div_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_add_pos_helper +norm_num.pos_bit0_helper +norm_num.pos_bit1_helper +norm_num.pos_mul_neg_helper +norm_num.sub_eq_add_neg_helper norm_num.subst_into_div -norm_num.nonzero_of_div_helper -norm_num.neg_zero_helper +norm_num.subst_into_prod +norm_num.subst_into_subtr +norm_num.subst_into_sum +not +not_of_iff_false +not_of_not_not_not num -num.zero num.pos +num.zero of_iff_true one one_mul option -option.some option.none +option.some or or.elim or.intro_left or.intro_right +or.neg_resolve_left +or.neg_resolve_right or.rec or.resolve_left or.resolve_right -or.neg_resolve_left -or.neg_resolve_right poly_unit poly_unit.star pos_num -pos_num.one pos_num.bit0 pos_num.bit1 +pos_num.one prod prod.mk prod.pr1 @@ -173,8 +175,8 @@ prod.pr2 propext rat.divide rat.of_num -ring right_distrib +ring semiring sigma sigma.mk @@ -187,13 +189,10 @@ subsingleton subsingleton.elim tactic tactic.all_goals -tactic.apply -tactic.assert_hypothesis -tactic.eapply -tactic.fapply -tactic.eassumption tactic.and_then tactic.append +tactic.apply +tactic.assert_hypothesis tactic.assumption tactic.at_most tactic.beta @@ -205,30 +204,32 @@ tactic.clear tactic.clears tactic.determ tactic.discard -tactic.intro -tactic.intros +tactic.eapply +tactic.eassumption tactic.exact tactic.expr tactic.expr.builtin tactic.expr_list tactic.expr_list.cons tactic.expr_list.nil -tactic.using_expr -tactic.none_expr -tactic.identifier -tactic.identifier_list -tactic.opt_expr -tactic.opt_identifier_list tactic.fail +tactic.fapply tactic.fixpoint tactic.focus_at -tactic.generalize_tac tactic.generalizes +tactic.generalize_tac tactic.id +tactic.identifier +tactic.identifier_list tactic.interleave +tactic.intro +tactic.intros tactic.lettac +tactic.none_expr tactic.now +tactic.opt_expr tactic.opt_expr_list +tactic.opt_identifier_list tactic.or_else tactic.par tactic.refine @@ -242,16 +243,15 @@ tactic.rotate_right tactic.state tactic.trace tactic.try_for +tactic.using_expr tactic.whnf trans_rel_left trans_rel_right true true.intro -is_trunc.is_hset -is_trunc.is_hprop weak_order well_founded zero -zero_mul zero_le_one zero_lt_one +zero_mul