chore(library/constants): sort constant decls
This commit is contained in:
Leonardo de Moura
parent
193a9d8cde
commit
95fba3dba6
3 changed files with 420 additions and 420 deletions
File diff suppressed because it is too large
Load diff
|
|
@ -9,8 +9,8 @@ name const & get_absurd_name();
|
||||||
name const & get_add_name();
|
name const & get_add_name();
|
||||||
name const & get_add_comm_group_name();
|
name const & get_add_comm_group_name();
|
||||||
name const & get_add_comm_semigroup_name();
|
name const & get_add_comm_semigroup_name();
|
||||||
name const & get_add_monoid_name();
|
|
||||||
name const & get_add_group_name();
|
name const & get_add_group_name();
|
||||||
|
name const & get_add_monoid_name();
|
||||||
name const & get_and_name();
|
name const & get_and_name();
|
||||||
name const & get_and_elim_left_name();
|
name const & get_and_elim_left_name();
|
||||||
name const & get_and_elim_right_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_name();
|
||||||
name const & get_empty_rec_name();
|
name const & get_empty_rec_name();
|
||||||
name const & get_eq_name();
|
name const & get_eq_name();
|
||||||
|
name const & get_eq_drec_name();
|
||||||
name const & get_eq_elim_inv_inv_name();
|
name const & get_eq_elim_inv_inv_name();
|
||||||
name const & get_eq_intro_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_mp_name();
|
||||||
name const & get_eq_mpr_name();
|
name const & get_eq_mpr_name();
|
||||||
name const & get_eq_nrec_name();
|
name const & get_eq_nrec_name();
|
||||||
|
name const & get_eq_rec_name();
|
||||||
name const & get_eq_rec_eq_name();
|
name const & get_eq_rec_eq_name();
|
||||||
name const & get_eq_refl_name();
|
name const & get_eq_refl_name();
|
||||||
|
name const & get_eq_subst_name();
|
||||||
name const & get_eq_symm_name();
|
name const & get_eq_symm_name();
|
||||||
name const & get_eq_trans_name();
|
name const & get_eq_trans_name();
|
||||||
name const & get_eq_subst_name();
|
|
||||||
name const & get_exists_elim_name();
|
name const & get_exists_elim_name();
|
||||||
name const & get_false_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_of_true_iff_false_name();
|
||||||
|
name const & get_false_rec_name();
|
||||||
name const & get_field_name();
|
name const & get_field_name();
|
||||||
name const & get_funext_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_add_name();
|
||||||
name const & get_has_div_name();
|
name const & get_has_div_name();
|
||||||
name const & get_has_mul_name();
|
name const & get_has_mul_name();
|
||||||
name const & get_has_neg_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_sub_name();
|
||||||
|
name const & get_has_zero_name();
|
||||||
|
name const & get_has_zero_zero_name();
|
||||||
name const & get_heq_name();
|
name const & get_heq_name();
|
||||||
name const & get_heq_refl_name();
|
name const & get_heq_refl_name();
|
||||||
name const & get_heq_to_eq_name();
|
name const & get_heq_to_eq_name();
|
||||||
name const & get_iff_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_left_name();
|
||||||
name const & get_iff_elim_right_name();
|
name const & get_iff_elim_right_name();
|
||||||
name const & get_iff_false_intro_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_iff_true_intro_name();
|
||||||
name const & get_implies_resolve_name();
|
|
||||||
name const & get_implies_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_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_hprop_elim_name();
|
||||||
|
name const & get_is_trunc_is_hset_name();
|
||||||
name const & get_ite_name();
|
name const & get_ite_name();
|
||||||
name const & get_le_refl_name();
|
|
||||||
name const & get_left_distrib_name();
|
name const & get_left_distrib_name();
|
||||||
name const & get_linear_ordered_semiring_name();
|
name const & get_le_refl_name();
|
||||||
name const & get_linear_ordered_ring_name();
|
|
||||||
name const & get_lift_name();
|
name const & get_lift_name();
|
||||||
name const & get_lift_down_name();
|
name const & get_lift_down_name();
|
||||||
name const & get_lift_up_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_monoid_name();
|
||||||
name const & get_mul_name();
|
name const & get_mul_name();
|
||||||
name const & get_mul_one_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_name();
|
||||||
|
name const & get_mul_zero_class_name();
|
||||||
name const & get_nat_name();
|
name const & get_nat_name();
|
||||||
name const & get_nat_of_num_name();
|
name const & get_nat_of_num_name();
|
||||||
name const & get_nat_succ_name();
|
name const & get_nat_succ_name();
|
||||||
name const & get_nat_zero_name();
|
name const & get_nat_zero_name();
|
||||||
name const & get_ne_name();
|
name const & get_ne_name();
|
||||||
name const & get_neg_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_name();
|
||||||
name const & get_norm_num_add1_bit0_name();
|
name const & get_norm_num_add1_bit0_name();
|
||||||
name const & get_norm_num_add1_bit1_helper_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_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_add_zero_name();
|
||||||
name const & get_norm_num_bin_zero_add_name();
|
name const & get_norm_num_bin_zero_add_name();
|
||||||
name const & get_norm_num_bit0_add_bit0_helper_name();
|
name const & get_norm_num_bit0_add_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_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_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_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_mk_cong_name();
|
||||||
name const & get_norm_num_mul_bit0_helper_name();
|
name const & get_norm_num_mul_bit0_helper_name();
|
||||||
name const & get_norm_num_mul_bit1_helper_name();
|
name const & get_norm_num_mul_bit1_helper_name();
|
||||||
name const & get_norm_num_one_add_bit1_helper_name();
|
name const & get_norm_num_mul_div_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_neg_add_neg_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_helper1_name();
|
||||||
name const & get_norm_num_neg_add_pos_helper2_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_neg_helper_name();
|
||||||
name const & get_norm_num_neg_mul_pos_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_neg_neg_helper_name();
|
||||||
name const & get_norm_num_add_div_helper_name();
|
name const & get_norm_num_neg_zero_helper_name();
|
||||||
name const & get_norm_num_div_add_helper_name();
|
|
||||||
name const & get_norm_num_nonneg_bit0_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_nonneg_bit1_helper_name();
|
||||||
name const & get_norm_num_pos_bit0_helper_name();
|
name const & get_norm_num_nonzero_of_div_helper_name();
|
||||||
name const & get_norm_num_pos_bit1_helper_name();
|
|
||||||
name const & get_norm_num_nonzero_of_neg_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_nonzero_of_pos_helper_name();
|
||||||
name const & get_norm_num_mul_div_helper_name();
|
name const & get_norm_num_one_add_bit0_name();
|
||||||
name const & get_norm_num_div_mul_helper_name();
|
name const & get_norm_num_one_add_bit1_helper_name();
|
||||||
name const & get_norm_num_div_helper_name();
|
name const & get_norm_num_one_add_one_name();
|
||||||
name const & get_norm_num_div_eq_div_helper_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_subst_into_div_name();
|
||||||
name const & get_norm_num_nonzero_of_div_helper_name();
|
name const & get_norm_num_subst_into_prod_name();
|
||||||
name const & get_norm_num_neg_zero_helper_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_name();
|
||||||
name const & get_num_zero_name();
|
|
||||||
name const & get_num_pos_name();
|
name const & get_num_pos_name();
|
||||||
|
name const & get_num_zero_name();
|
||||||
name const & get_of_iff_true_name();
|
name const & get_of_iff_true_name();
|
||||||
name const & get_one_name();
|
name const & get_one_name();
|
||||||
name const & get_one_mul_name();
|
name const & get_one_mul_name();
|
||||||
name const & get_option_name();
|
name const & get_option_name();
|
||||||
name const & get_option_some_name();
|
|
||||||
name const & get_option_none_name();
|
name const & get_option_none_name();
|
||||||
|
name const & get_option_some_name();
|
||||||
name const & get_or_name();
|
name const & get_or_name();
|
||||||
name const & get_or_elim_name();
|
name const & get_or_elim_name();
|
||||||
name const & get_or_intro_left_name();
|
name const & get_or_intro_left_name();
|
||||||
name const & get_or_intro_right_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_rec_name();
|
||||||
name const & get_or_resolve_left_name();
|
name const & get_or_resolve_left_name();
|
||||||
name const & get_or_resolve_right_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_name();
|
||||||
name const & get_poly_unit_star_name();
|
name const & get_poly_unit_star_name();
|
||||||
name const & get_pos_num_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_bit0_name();
|
||||||
name const & get_pos_num_bit1_name();
|
name const & get_pos_num_bit1_name();
|
||||||
|
name const & get_pos_num_one_name();
|
||||||
name const & get_prod_name();
|
name const & get_prod_name();
|
||||||
name const & get_prod_mk_name();
|
name const & get_prod_mk_name();
|
||||||
name const & get_prod_pr1_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_propext_name();
|
||||||
name const & get_rat_divide_name();
|
name const & get_rat_divide_name();
|
||||||
name const & get_rat_of_num_name();
|
name const & get_rat_of_num_name();
|
||||||
name const & get_ring_name();
|
|
||||||
name const & get_right_distrib_name();
|
name const & get_right_distrib_name();
|
||||||
|
name const & get_ring_name();
|
||||||
name const & get_semiring_name();
|
name const & get_semiring_name();
|
||||||
name const & get_sigma_name();
|
name const & get_sigma_name();
|
||||||
name const & get_sigma_mk_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_subsingleton_elim_name();
|
||||||
name const & get_tactic_name();
|
name const & get_tactic_name();
|
||||||
name const & get_tactic_all_goals_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_and_then_name();
|
||||||
name const & get_tactic_append_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_assumption_name();
|
||||||
name const & get_tactic_at_most_name();
|
name const & get_tactic_at_most_name();
|
||||||
name const & get_tactic_beta_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_clears_name();
|
||||||
name const & get_tactic_determ_name();
|
name const & get_tactic_determ_name();
|
||||||
name const & get_tactic_discard_name();
|
name const & get_tactic_discard_name();
|
||||||
name const & get_tactic_intro_name();
|
name const & get_tactic_eapply_name();
|
||||||
name const & get_tactic_intros_name();
|
name const & get_tactic_eassumption_name();
|
||||||
name const & get_tactic_exact_name();
|
name const & get_tactic_exact_name();
|
||||||
name const & get_tactic_expr_name();
|
name const & get_tactic_expr_name();
|
||||||
name const & get_tactic_expr_builtin_name();
|
name const & get_tactic_expr_builtin_name();
|
||||||
name const & get_tactic_expr_list_name();
|
name const & get_tactic_expr_list_name();
|
||||||
name const & get_tactic_expr_list_cons_name();
|
name const & get_tactic_expr_list_cons_name();
|
||||||
name const & get_tactic_expr_list_nil_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_fail_name();
|
||||||
|
name const & get_tactic_fapply_name();
|
||||||
name const & get_tactic_fixpoint_name();
|
name const & get_tactic_fixpoint_name();
|
||||||
name const & get_tactic_focus_at_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_generalizes_name();
|
||||||
|
name const & get_tactic_generalize_tac_name();
|
||||||
name const & get_tactic_id_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_interleave_name();
|
||||||
|
name const & get_tactic_intro_name();
|
||||||
|
name const & get_tactic_intros_name();
|
||||||
name const & get_tactic_lettac_name();
|
name const & get_tactic_lettac_name();
|
||||||
|
name const & get_tactic_none_expr_name();
|
||||||
name const & get_tactic_now_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_expr_list_name();
|
||||||
|
name const & get_tactic_opt_identifier_list_name();
|
||||||
name const & get_tactic_or_else_name();
|
name const & get_tactic_or_else_name();
|
||||||
name const & get_tactic_par_name();
|
name const & get_tactic_par_name();
|
||||||
name const & get_tactic_refine_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_state_name();
|
||||||
name const & get_tactic_trace_name();
|
name const & get_tactic_trace_name();
|
||||||
name const & get_tactic_try_for_name();
|
name const & get_tactic_try_for_name();
|
||||||
|
name const & get_tactic_using_expr_name();
|
||||||
name const & get_tactic_whnf_name();
|
name const & get_tactic_whnf_name();
|
||||||
name const & get_trans_rel_left_name();
|
name const & get_trans_rel_left_name();
|
||||||
name const & get_trans_rel_right_name();
|
name const & get_trans_rel_right_name();
|
||||||
name const & get_true_name();
|
name const & get_true_name();
|
||||||
name const & get_true_intro_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_weak_order_name();
|
||||||
name const & get_well_founded_name();
|
name const & get_well_founded_name();
|
||||||
name const & get_zero_name();
|
name const & get_zero_name();
|
||||||
name const & get_zero_mul_name();
|
|
||||||
name const & get_zero_le_one_name();
|
name const & get_zero_le_one_name();
|
||||||
name const & get_zero_lt_one_name();
|
name const & get_zero_lt_one_name();
|
||||||
|
name const & get_zero_mul_name();
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -2,8 +2,8 @@ absurd
|
||||||
add
|
add
|
||||||
add_comm_group
|
add_comm_group
|
||||||
add_comm_semigroup
|
add_comm_semigroup
|
||||||
add_monoid
|
|
||||||
add_group
|
add_group
|
||||||
|
add_monoid
|
||||||
and
|
and
|
||||||
and.elim_left
|
and.elim_left
|
||||||
and.elim_right
|
and.elim_right
|
||||||
|
|
@ -27,145 +27,147 @@ div
|
||||||
empty
|
empty
|
||||||
empty.rec
|
empty.rec
|
||||||
eq
|
eq
|
||||||
|
eq.drec
|
||||||
eq.elim_inv_inv
|
eq.elim_inv_inv
|
||||||
eq.intro
|
eq.intro
|
||||||
eq.rec
|
|
||||||
eq.drec
|
|
||||||
eq.mp
|
eq.mp
|
||||||
eq.mpr
|
eq.mpr
|
||||||
eq.nrec
|
eq.nrec
|
||||||
|
eq.rec
|
||||||
eq_rec_eq
|
eq_rec_eq
|
||||||
eq.refl
|
eq.refl
|
||||||
|
eq.subst
|
||||||
eq.symm
|
eq.symm
|
||||||
eq.trans
|
eq.trans
|
||||||
eq.subst
|
|
||||||
exists.elim
|
exists.elim
|
||||||
false
|
false
|
||||||
false.rec
|
|
||||||
false_of_true_iff_false
|
false_of_true_iff_false
|
||||||
|
false.rec
|
||||||
field
|
field
|
||||||
funext
|
funext
|
||||||
has_zero
|
|
||||||
has_one
|
|
||||||
has_zero.zero
|
|
||||||
has_one.one
|
|
||||||
has_add
|
has_add
|
||||||
has_div
|
has_div
|
||||||
has_mul
|
has_mul
|
||||||
has_neg
|
has_neg
|
||||||
|
has_one
|
||||||
|
has_one.one
|
||||||
has_sub
|
has_sub
|
||||||
|
has_zero
|
||||||
|
has_zero.zero
|
||||||
heq
|
heq
|
||||||
heq.refl
|
heq.refl
|
||||||
heq.to_eq
|
heq.to_eq
|
||||||
iff
|
iff
|
||||||
iff.refl
|
|
||||||
iff.symm
|
|
||||||
iff.trans
|
|
||||||
iff.mp
|
|
||||||
iff.mpr
|
|
||||||
iff.intro
|
|
||||||
iff.elim_left
|
iff.elim_left
|
||||||
iff.elim_right
|
iff.elim_right
|
||||||
iff_false_intro
|
iff_false_intro
|
||||||
|
iff.intro
|
||||||
|
iff.mp
|
||||||
|
iff.mpr
|
||||||
|
iff.refl
|
||||||
|
iff.symm
|
||||||
|
iff.trans
|
||||||
iff_true_intro
|
iff_true_intro
|
||||||
implies.resolve
|
|
||||||
implies
|
implies
|
||||||
implies_of_if_pos
|
|
||||||
implies_of_if_neg
|
implies_of_if_neg
|
||||||
|
implies_of_if_pos
|
||||||
|
implies.resolve
|
||||||
|
is_trunc.is_hprop
|
||||||
is_trunc.is_hprop.elim
|
is_trunc.is_hprop.elim
|
||||||
|
is_trunc.is_hset
|
||||||
ite
|
ite
|
||||||
le.refl
|
|
||||||
left_distrib
|
left_distrib
|
||||||
linear_ordered_semiring
|
le.refl
|
||||||
linear_ordered_ring
|
|
||||||
lift
|
lift
|
||||||
lift.down
|
lift.down
|
||||||
lift.up
|
lift.up
|
||||||
|
linear_ordered_ring
|
||||||
|
linear_ordered_semiring
|
||||||
monoid
|
monoid
|
||||||
mul
|
mul
|
||||||
mul_one
|
mul_one
|
||||||
mul_zero_class
|
|
||||||
mul_zero
|
mul_zero
|
||||||
|
mul_zero_class
|
||||||
nat
|
nat
|
||||||
nat.of_num
|
nat.of_num
|
||||||
nat.succ
|
nat.succ
|
||||||
nat.zero
|
nat.zero
|
||||||
ne
|
ne
|
||||||
neg
|
neg
|
||||||
not
|
|
||||||
not_of_iff_false
|
|
||||||
not_of_not_not_not
|
|
||||||
norm_num.add1
|
norm_num.add1
|
||||||
norm_num.add1_bit0
|
norm_num.add1_bit0
|
||||||
norm_num.add1_bit1_helper
|
norm_num.add1_bit1_helper
|
||||||
norm_num.add1_zero
|
|
||||||
norm_num.add1_one
|
norm_num.add1_one
|
||||||
|
norm_num.add1_zero
|
||||||
|
norm_num.add_div_helper
|
||||||
norm_num.bin_add_zero
|
norm_num.bin_add_zero
|
||||||
norm_num.bin_zero_add
|
norm_num.bin_zero_add
|
||||||
norm_num.bit0_add_bit0_helper
|
norm_num.bit0_add_bit0_helper
|
||||||
norm_num.bit1_add_bit0_helper
|
|
||||||
norm_num.bit0_add_bit1_helper
|
norm_num.bit0_add_bit1_helper
|
||||||
norm_num.bit1_add_bit1_helper
|
|
||||||
norm_num.bit0_add_one
|
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.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.mk_cong
|
||||||
norm_num.mul_bit0_helper
|
norm_num.mul_bit0_helper
|
||||||
norm_num.mul_bit1_helper
|
norm_num.mul_bit1_helper
|
||||||
norm_num.one_add_bit1_helper
|
norm_num.mul_div_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.neg_add_neg_helper
|
norm_num.neg_add_neg_helper
|
||||||
norm_num.neg_add_pos_helper1
|
norm_num.neg_add_pos_helper1
|
||||||
norm_num.neg_add_pos_helper2
|
norm_num.neg_add_pos_helper2
|
||||||
norm_num.pos_add_neg_helper
|
|
||||||
norm_num.neg_mul_neg_helper
|
norm_num.neg_mul_neg_helper
|
||||||
norm_num.neg_mul_pos_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.neg_neg_helper
|
||||||
norm_num.add_div_helper
|
norm_num.neg_zero_helper
|
||||||
norm_num.div_add_helper
|
|
||||||
norm_num.nonneg_bit0_helper
|
norm_num.nonneg_bit0_helper
|
||||||
norm_num.nonneg_bit1_helper
|
norm_num.nonneg_bit1_helper
|
||||||
norm_num.pos_bit0_helper
|
norm_num.nonzero_of_div_helper
|
||||||
norm_num.pos_bit1_helper
|
|
||||||
norm_num.nonzero_of_neg_helper
|
norm_num.nonzero_of_neg_helper
|
||||||
norm_num.nonzero_of_pos_helper
|
norm_num.nonzero_of_pos_helper
|
||||||
norm_num.mul_div_helper
|
norm_num.one_add_bit0
|
||||||
norm_num.div_mul_helper
|
norm_num.one_add_bit1_helper
|
||||||
norm_num.div_helper
|
norm_num.one_add_one
|
||||||
norm_num.div_eq_div_helper
|
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.subst_into_div
|
||||||
norm_num.nonzero_of_div_helper
|
norm_num.subst_into_prod
|
||||||
norm_num.neg_zero_helper
|
norm_num.subst_into_subtr
|
||||||
|
norm_num.subst_into_sum
|
||||||
|
not
|
||||||
|
not_of_iff_false
|
||||||
|
not_of_not_not_not
|
||||||
num
|
num
|
||||||
num.zero
|
|
||||||
num.pos
|
num.pos
|
||||||
|
num.zero
|
||||||
of_iff_true
|
of_iff_true
|
||||||
one
|
one
|
||||||
one_mul
|
one_mul
|
||||||
option
|
option
|
||||||
option.some
|
|
||||||
option.none
|
option.none
|
||||||
|
option.some
|
||||||
or
|
or
|
||||||
or.elim
|
or.elim
|
||||||
or.intro_left
|
or.intro_left
|
||||||
or.intro_right
|
or.intro_right
|
||||||
|
or.neg_resolve_left
|
||||||
|
or.neg_resolve_right
|
||||||
or.rec
|
or.rec
|
||||||
or.resolve_left
|
or.resolve_left
|
||||||
or.resolve_right
|
or.resolve_right
|
||||||
or.neg_resolve_left
|
|
||||||
or.neg_resolve_right
|
|
||||||
poly_unit
|
poly_unit
|
||||||
poly_unit.star
|
poly_unit.star
|
||||||
pos_num
|
pos_num
|
||||||
pos_num.one
|
|
||||||
pos_num.bit0
|
pos_num.bit0
|
||||||
pos_num.bit1
|
pos_num.bit1
|
||||||
|
pos_num.one
|
||||||
prod
|
prod
|
||||||
prod.mk
|
prod.mk
|
||||||
prod.pr1
|
prod.pr1
|
||||||
|
|
@ -173,8 +175,8 @@ prod.pr2
|
||||||
propext
|
propext
|
||||||
rat.divide
|
rat.divide
|
||||||
rat.of_num
|
rat.of_num
|
||||||
ring
|
|
||||||
right_distrib
|
right_distrib
|
||||||
|
ring
|
||||||
semiring
|
semiring
|
||||||
sigma
|
sigma
|
||||||
sigma.mk
|
sigma.mk
|
||||||
|
|
@ -187,13 +189,10 @@ subsingleton
|
||||||
subsingleton.elim
|
subsingleton.elim
|
||||||
tactic
|
tactic
|
||||||
tactic.all_goals
|
tactic.all_goals
|
||||||
tactic.apply
|
|
||||||
tactic.assert_hypothesis
|
|
||||||
tactic.eapply
|
|
||||||
tactic.fapply
|
|
||||||
tactic.eassumption
|
|
||||||
tactic.and_then
|
tactic.and_then
|
||||||
tactic.append
|
tactic.append
|
||||||
|
tactic.apply
|
||||||
|
tactic.assert_hypothesis
|
||||||
tactic.assumption
|
tactic.assumption
|
||||||
tactic.at_most
|
tactic.at_most
|
||||||
tactic.beta
|
tactic.beta
|
||||||
|
|
@ -205,30 +204,32 @@ tactic.clear
|
||||||
tactic.clears
|
tactic.clears
|
||||||
tactic.determ
|
tactic.determ
|
||||||
tactic.discard
|
tactic.discard
|
||||||
tactic.intro
|
tactic.eapply
|
||||||
tactic.intros
|
tactic.eassumption
|
||||||
tactic.exact
|
tactic.exact
|
||||||
tactic.expr
|
tactic.expr
|
||||||
tactic.expr.builtin
|
tactic.expr.builtin
|
||||||
tactic.expr_list
|
tactic.expr_list
|
||||||
tactic.expr_list.cons
|
tactic.expr_list.cons
|
||||||
tactic.expr_list.nil
|
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.fail
|
||||||
|
tactic.fapply
|
||||||
tactic.fixpoint
|
tactic.fixpoint
|
||||||
tactic.focus_at
|
tactic.focus_at
|
||||||
tactic.generalize_tac
|
|
||||||
tactic.generalizes
|
tactic.generalizes
|
||||||
|
tactic.generalize_tac
|
||||||
tactic.id
|
tactic.id
|
||||||
|
tactic.identifier
|
||||||
|
tactic.identifier_list
|
||||||
tactic.interleave
|
tactic.interleave
|
||||||
|
tactic.intro
|
||||||
|
tactic.intros
|
||||||
tactic.lettac
|
tactic.lettac
|
||||||
|
tactic.none_expr
|
||||||
tactic.now
|
tactic.now
|
||||||
|
tactic.opt_expr
|
||||||
tactic.opt_expr_list
|
tactic.opt_expr_list
|
||||||
|
tactic.opt_identifier_list
|
||||||
tactic.or_else
|
tactic.or_else
|
||||||
tactic.par
|
tactic.par
|
||||||
tactic.refine
|
tactic.refine
|
||||||
|
|
@ -242,16 +243,15 @@ tactic.rotate_right
|
||||||
tactic.state
|
tactic.state
|
||||||
tactic.trace
|
tactic.trace
|
||||||
tactic.try_for
|
tactic.try_for
|
||||||
|
tactic.using_expr
|
||||||
tactic.whnf
|
tactic.whnf
|
||||||
trans_rel_left
|
trans_rel_left
|
||||||
trans_rel_right
|
trans_rel_right
|
||||||
true
|
true
|
||||||
true.intro
|
true.intro
|
||||||
is_trunc.is_hset
|
|
||||||
is_trunc.is_hprop
|
|
||||||
weak_order
|
weak_order
|
||||||
well_founded
|
well_founded
|
||||||
zero
|
zero
|
||||||
zero_mul
|
|
||||||
zero_le_one
|
zero_le_one
|
||||||
zero_lt_one
|
zero_lt_one
|
||||||
|
zero_mul
|
||||||
|
|
|
||||||
Loading…
Reference in a new issue