coq.txt

UltraEdit中几百种语法高亮度显示

div_continuity div_continuous div_eq_inv double_S double_even
double_odd double_var double_var
eps2 eps2_Rgt_R0 eps4 eqT_eq_bij eq_IZR eq_IZR_R0 eq_Rge eq_Rge_sym eq_Rle
eq_Rle_sym eq_Rminus eq_Ropp eq_RoppO eq_add_S eq_dep1_dep eq_dep1_eq
eq_dep_dep1 eq_dep_eq eq_dep_sym eq_dep_trans eq_eqT_bij eq_eq_nat eq_fct eq_le
eq_lt_x_Sy eq_nat_dec eq_nat_decide eq_nat_elim eq_nat_eq eq_nat_refl eq_not_lt
eq_not_neq_y_x eq_proofs_unicity eq_true_false_abs eqb_eq eqb_negb1
eqb_negb2 eqb_prop eqb_refl eqb_reflx eqb_subst eqf_refl eqf_sym eqf_trans
eqf_xor_1 eqm_refl eqm_sym eqm_trans eqmap_refl eqmap_sym eqmap_trans eqst_ntheq
equiv_eqex_eqdep eucl_dev even_2n even_div2 even_double even_even_plus
even_mult_aux even_mult_inv_l even_mult_inv_r even_mult_l even_mult_r
even_odd_dec even_odd_div2 even_odd_double even_or_odd even_plus_aux
even_plus_even_inv_l even_plus_even_inv_r even_plus_odd_inv_l
even_plus_odd_inv_r event_O ex_not_not_all ex_not_not_all exists_S_le
exists_in_int exists_le_S exists_lt
f_equal f_equal2 f_equal3 f_equal4 f_equal5 fact_neq_0 false_xorb
finite_cardinal finite_greater finite_image fix_eq floor_gt0 floor_ok
fold_right_aapp fold_symmetric for_base_fp form1 form2 form3 form4 fp_R0 fp_nat
fst_nth_nth
ge0_plus_ge0_is_ge0 ge0_plus_gt0_is_gt0 gen growing_prop gt0_plus_ge0_is_gt0
gt0_plus_gt0_is_gt0 gt_O_eq gt_S gt_S_le gt_S_n gt_Sn_O gt_Sn_n gt_antirefl
gt_eq_gt_dec gt_le_S gt_le_trans gt_n_S gt_not_sym gt_pred gt_reg_l
gt_trans gt_trans_S gt_wf_ind gt_wf_rec
heap_to_list
idempot_rev if_negb ifdec_left ifdec_right iff_refl iff_sym iff_trans
image_empty imp_not_Req imp_simp imply_and_or imply_and_or2 imply_to_and
imply_to_or in_FSet_delta in_FSet_diff in_FSet_inter in_FSet_union in_app_or
in_app_or in_cons in_cons in_dom_DMerge_1 in_dom_DMerge_2 in_dom_DMerge_3
in_dom_M0 in_dom_M1 in_dom_M1_1 in_dom_M1_2 in_dom_delta in_dom_merge
in_dom_none in_dom_put in_dom_put_behind in_dom_remove in_dom_restrby
in_dom_restrto in_dom_some in_eq in_eq in_int_S in_int_Sp_q in_int_between
in_int_exists in_int_intro in_int_lt in_int_p_Sq in_inv in_map in_nil in_or_app
in_or_app in_prod in_prod_aux incl_add incl_add_x incl_app incl_app incl_appl
incl_appl incl_appr incl_appr incl_card_le incl_clos_trans incl_cons incl_cons
incl_left incl_refl incl_refl incl_right incl_soustr incl_soustr_add_l
incl_soustr_add_r incl_soustr_in incl_st_add_soustr incl_st_card_lt incl_tl
incl_tl incl_tran incl_tran increasing_decreasing increasing_decreasing_opp
ind_0_1_SS induction_gtof1 induction_gtof2 induction_ltof1 induction_ltof2
inh_card_gt_O inj_S inj_eq inj_ge inj_gt inj_le inj_lt inj_minus1 inj_minus2
inj_minus_aux inj_mult inj_neq inj_pair2 inj_plus inj_right_pair
inject_nat_complete inject_nat_complete_inf inject_nat_prop inject_nat_set
injective_preserves_cardinal inser_trans_R insert inst interval_split intro_Z
inv_continuity inv_continuous inverse_image_of_eq inverse_image_of_equivalence
invert_heap is_double_moins_un is_heap_rec isometric_rot_trans
isometric_rotation isometric_rotation_0 isometric_trans_rot
isometric_translation iter_convert iter_nat_invariant iter_nat_plus iter_pos_add
iter_pos_invariant
law_cosines leA_Tree_Leaf leA_Tree_Node le_INR le_IZR le_IZR_R1 le_O_IZR le_O_n
le_Order le_S_compat le_S_gt le_S_n le_Sn_O le_Sn_n le_Sx_y_lt le_add_compat
le_add_compat_l le_add_compat_r le_antisym le_antisym le_dec le_decide
le_elim_rel le_epsilon le_eq_compat le_ge_dec le_gt_S le_gt_dec le_gt_trans
le_le_S_dec le_le_S_eq le_le_x_Sy le_lt_dec le_lt_eq_dec le_lt_n_Sm le_lt_or_eq
le_lt_plus_plus le_lt_trans le_lt_trans le_lt_x_Sy le_max_l le_max_r le_min_l
le_min_r le_minus le_n_O_eq le_n_S le_n_Sn le_ni_le le_not_gt le_not_lt le_or_lt
le_plus_l le_plus_minus le_plus_minus_r le_plus_plus le_plus_r le_plus_trans
le_pred_n le_reflexive le_reg_l le_reg_r le_total_order le_trans le_trans
le_trans le_trans_S leb_refl left_prefix lel_cons lel_cons lel_cons_cons
lel_cons_cons lel_nil lel_nil lel_refl lel_refl lel_tail lel_tail lel_trans
lel_trans lelistA_inv length_as_fold length_as_fold_2 less_than_empty
less_than_singleton lim_x limit_Ropp limit_comp limit_free limit_inv limit_minus
limit_mul limit_plus list_contents_app list_eq_dec list_to_heap log_inf_correct
log_inf_le_log_sup log_inf_shift_nat log_near_correct1 log_near_correct2
log_sup_correct1 log_sup_correct2 log_sup_le_Slog_inf log_sup_log_inf
log_sup_shift_nat low_trans lt_0_1 lt_INR lt_INR_0 lt_IZR lt_O_IZR lt_O_Sn
lt_O_minus_lt lt_O_neq lt_S lt_S_n lt_Sx_y_lt lt_add_compat lt_add_compat_r
lt_add_compat_weak_l lt_add_compat_weak_r lt_anti_sym lt_div2 lt_eq_lt_dec lt_le
lt_le_S lt_le_Sx_y lt_le_plus_plus lt_le_trans lt_le_trans lt_le_weak lt_lt_x_Sy
lt_minus lt_mult_left lt_n_O lt_n_S lt_n_Sm_le lt_n_Sn lt_n_n lt_neq lt_neq_sym
lt_not_le lt_not_sym lt_plus_plus lt_plus_trans lt_pred lt_pred_n_n lt_reg_l
lt_reg_r lt_wf lt_wf_double_ind lt_wf_double_rec lt_wf_ind lt_wf_rec
lt_wf_rec1 ltl_unit
makeM2_M2 makeM2_canon make_new_approximant map_dom_empty_1 map_dom_empty_2
mapcanon_M2 mapcanon_M2_1 mapcanon_M2_2 mapcanon_exists mapcanon_exists_1
mapcanon_exists_2 mapcanon_unique max_SS max_case max_case2 max_dec max_l max_r
max_sym meq_congr meq_left meq_refl meq_right meq_sym meq_trans merge min_SS
min_case min_case2 min_dec min_l min_r min_sym minus_INR minus_R0 minus_Rge
minus_Rgt minus_Sn_m minus_n_O minus_n_n minus_plus minus_plus_simpl modulo
mul_factor_gt mul_factor_gt_f mul_factor_wd mult_1_n mult_INR mult_IZR mult_O_le
mult_acc_aux mult_assoc_l mult_assoc_r mult_le mult_le_conv_1 mult_lt
mult_minus_distr mult_n_1 mult_n_O mult_n_Sm mult_non_zero mult_plus_distr
mult_plus_distr_r mult_sym mult_tail_mult multiset_twist1 multiset_twist2
munion_ass munion_comm munion_empty_left munion_empty_right munion_perm_left
munion_rotate
n_Sn nat_case nat_double_ind nat_le_complete nat_le_complete_conv nat_le_correct
nat_le_correct_conv nat_of_ad_double nat_of_ad_double_plus_un nat_of_ad_of_nat
nat_total_order natlike_ind natlike_rec neg_cos neg_pos_Rsqr_le neg_sin
negative_derivative negb_andb negb_elim negb_intro negb_orb negb_sym neq_0_1
neq_O_lt neq_antirefl neq_eq_compat neq_not_eq neq_not_eq_y_x
neq_x_Sx newMap_semantics new_var ni_le_antisym ni_le_le ni_le_min_1
ni_le_min_2 ni_le_min_induc ni_le_refl ni_le_total ni_le_trans ni_min_O_l
ni_min_O_r ni_min_assoc ni_min_case ni_min_comm ni_min_idemp ni_min_inf_l
ni_min_inf_r nil_cons nil_cons no_fixpoint_negb nonneg_derivative_0
nonpos_derivative_0 nonpos_derivative_1 not_1_INR not_Empty_Add not_INR_O
not_Isnil_cons not_O_INR not_O_IZR not_Req not_Rle not_SIncl_empty not_Zeq
not_Zge not_Zgt not_Zle not_Zlt not_all_ex_not not_all_ex_not not_all_not_ex
not_all_not_ex not_and not_and_or not_empty_Inhabited not_eq not_eq_S not_eq_sym
not_even_and_odd not_ex_all_not not_ex_all_not not_ex_not_all not_ex_not_all
not_false_is_true not_ge not_gt not_has_fixpoint not_imp not_imply_elim
not_imply_elim2 not_included_empty_Inhabited not_injective_elim not_le not_lt
not_neq_neq_trans not_nm_INR not_not not_or not_or_and not_sym not_true_is_false
nth_In nth_S_cons nth_in_or_default nth_le nth_le_length nth_lt_O ntheq_eqst
null_derivative_0 null_derivative_1
odd_S2n odd_div2 odd_double odd_even_plus odd_mult odd_mult_inv_l odd_mult_inv_r
odd_plus_even_inv_l odd_plus_even_inv_r odd_plus_l odd_plus_odd_inv_l
odd_plus_odd_inv_r odd_plus_r one_IZR_lt1 one_IZR_r_R1 op_rotate opp_continuity
opp_continuous opp_opp_fct opposite_derivable opposite_derivable_pt option_sum
or_not_and or_to_imply orb_assoc orb_b_false orb_b_true orb_false_b
orb_false_elim orb_false_intro orb_neg_b orb_prop orb_prop2 orb_sym orb_true_b
orb_true_elim orb_true_intro
pair_sp perm_left perm_right permut_app permut_cons permut_middle permut_refl
permut_right permut_tran plus_INR plus_IZR plus_IZR_NEG_POS plus_Int_part1
plus_Int_part2 plus_O_n plus_Sn_m plus_Snm_nSm plus_assoc_l plus_assoc_r
plus_frac_part1 plus_frac_part2 plus_is_O plus_is_one plus_le_is_le
plus_lt_is_lt plus_minus plus_n_O plus_n_Sm plus_permute plus_permute_2_in_4
plus_sym plus_tail_plus poly pos_INR pos_Rsqr pos_Rsqr1 positive_to_nat_2
positive_to_nat_4 positive_to_nat_mult pow_1 pow_O pow_R1 pow_RN_plus pow_add
pow_lt pow_lt_1_zero pow_ne_zero pow_nonzero powerRZ_1 powerRZ_NOR powerRZ_O
powerRZ_R1 powerRZ_add powerRZ_le powerRZ_lt pred_Sn pred_of_minus
prod_continuity prod_continuous prod_derivable prod_derivable_pt prod_neq_R0
proj1 proj2 prop_eps pythagorean
quotient
r_Rmult_mult r_Rplus_plus rad_deg rename retract_pow_U_U rev_ind right_prefix
rotation_0 rotation_PI2
same_relation_is_equivalence scal_continuity scal_continuous scal_derivable
scal_derivable_pt scal_derivable_pt_var seq_congr seq_left seq_refl seq_right
seq_sym seq_trans set_In_dec set_add_elim set_add_elim2 set_add_intro
set_add_intro1 set_add_intro2 set_add_not_empty set_diff_elim1 set_diff_elim2
set_diff_intro set_diff_trivial set_inter_elim set_inter_elim1 set_inter_elim2
set_inter_intro set_mem_complete1 set_mem_complete2 set_mem_correct1
set_mem_correct2 set_mem_ind set_mem_ind2 set_union_elim set_union_emptyL
set_union_emptyR set_union_intro set_union_intro1 set_union_intro2
setcover_intro setcover_inv shift_nat_correct shift_nat_plus shift_pos_correct
shift_pos_nat sigma_aux_inv sigma_diff sigma_diff_neg sigma_eq_arg sigma_first
sigma_last sigma_split simpl_add_l simpl_add_r simpl_fact simpl_gt_plus_l
simpl_le_plus_l simpl_lt_plus_l simpl_plus_l sin2 sin2_cos2 sin3PI4 sin_0
sin_2PI sin_2PI3 sin_2a sin_3PI2 sin_5PI4 sin_PI sin_PI3 sin_PI3_cos_PI6 sin_PI4
sin_PI6 sin_PI6_cos_PI3 sin_PI_x sin_cos sin_cos5PI4 sin_cos_PI4 sin_decr_0
sin_decr_1 sin_decreasing_0 sin_decreasing_1 sin_eq_0_0 sin_eq_0_1
sin_eq_O_2PI_0 sin_eq_O_2PI_1 sin_ge_0 sin_gt_0 sin_incr_0 sin_incr_1
sin_increasing_0 sin_increasing_1 sin_lb_ge_0 sin_le_0 sin_lt_0 sin_lt_0_var
sin_neg sin_period sin_shift sincl_add_x single_limit single_z_r_R1 singlx
sort_inv sort_rec sqr_pos sqrt2_neq_0 sqrt3_2_neq_0 sqrt_0 sqrt_1 sqrt_Rsqr
sqrt_Rsqr_abs sqrt_cauchy sqrt_def sqrt_div sqrt_eq_0 sqrt_inj sqrt_le_0
sqrt_le_1 sqrt_lem_0 sqrt_less sqrt_lt_0 sqrt_lt_1 sqrt_lt_R0 sqrt_more
sqrt_square sqrt_times sqtr_lem_1 star_monotone
strictincreasing_strictdecreasing_opp sub_add sub_add_one sub_pos_SUPERIEUR
sub_pos_x_x sum_continuity sum_continuous sum_derivable sum_derivable_pt
sum_derivable_pt_var sum_f_R0_triangle sum_fct_cte_derivable
sum_fct_cte_derivable_pt sum_fct_cte_derive_pt sum_inequa_Rle_lt sumbool_and
sumbool_not sumbool_of_bool sumbool_or swap_Acc sym_EqSt sym_eq sym_eqT sym_idT
sym_not_eq sym_not_eqT sym_not_idT
tan_0 tan_2PI tan_2PI3 tan_2a tan_PI tan_PI3 tan_PI4 tan_PI6 tan_diff tan_gt_0
tan_incr_0 tan_incr_1 tan_increasing_0 tan_increasing_1 tan_lt_0 tan_minus
tan_neg tan_plus tech_Rgt_minus tech_Rplus tech_limit tech_limit_contr
tech_pow_Rmult tech_pow_Rplus tech_single_z_r_R1 tech_up times1_convert
times_add_distr times_assoc times_convert times_sym times_true_sub_distr
tl_nth_tl toRad_inj total_order total_order_Rge total_order_Rgt total_order_Rle
total_order_Rle_Rlt_eq total_order_Rlt total_order_Rlt_Rle trans_EqSt trans_eq
trans_eqT trans_idT translation_0 treesort treesort_twist1 treesort_twist1
treesort_twist2 treesort_twist2 triangle triangle_rectangle
triangle_rectangle_le triangle_rectangle_lt triv_nat true_sub_convert true_xorb
twist two_or_two_plus_one two_p_S two_p_gt_ZERO two_p_is_exp two_p_pred
two_power_nat_S two_power_nat_correct two_power_pos_correct two_power_pos_is_exp
two_power_pos_nat
unfold_Stream union_ass union_comm union_empty_left union_empty_right
union_perm_left union_rotate uniset_twist1 uniset_twist2 up_tech
weak_Zcompare_Zplus_compatible weak_Zmult_plus_distr_r weak_assoc
weaken_Zcompare_Zplus_compatible well_founded_gtof well_founded_ind
well_founded_induction well_founded_induction_type well_founded_lt_compat
well_founded_ltof wf_WO wf_clos_trans wf_disjoint_sum wf_incl wf_inverse_image
wf_lex_exp wf_lexprod wf_swapprod wf_symprod wf_union without_div_O_contr
without_div_Od without_div_Oi without_div_Oi1 without_div_Oi2
xorb_assoc xorb_comm xorb_eq xorb_false xorb_move_l_r_1 xorb_move_l_r_2
xorb_move_r_l_1 xorb_move_r_l_2 xorb_nilpotent xorb_true
zerob_false_elim zerob_false_intro zerob_true_elim zerob_true_intro zerop
ALL ALLT AC AC_IF Acc_clos_trans Acc_incl Acc_inv Acc_inv_trans Acc_inverse_image
Acc_swapprod Acc_symprod Acc_union Add_commutative Add_commutative' Add_covers
Add_distributes Add_intro1 Add_intro2 Add_inv Add_not_Empty Add_preserves_Finite
Alembert_exp Assoc
COS COS_bound Choice Choice2 Complement_Complement Couple_as_union Couple_inv
D_pow_n Dadd Dcomp Dcompare Dcompare_inf Dconst Diagram Distributivity
Distributivity' Dminus Dmult Dmult_const Dopp Dx Dx_pow_n
EX EXT EUn_noempty Elems_app Elems_canon Elems_of_list_of_dom Elems_of_list_of_dom_c
Elems_rev Empty_set_is_Bottom Empty_set_minimal Empty_set_zero Empty_set_zero'
EqSt_reflex Equiv_from_order Equiv_from_preorder Extension
FSetDelta_assoc FSetDelta_assoc_c FSetInter_M0_s FSetInter_M0_s_c
FSetInter_Union_l FSetInter_Union_l_c FSetInter_Union_r FSetInter_Union_r
FSetInter_assoc FSetInter_assoc_c FSetInter_comm FSetInter_comm_c
FSetInter_idempotent FSetInter_idempotent FSetInter_s_M0 FSetInter_s_M0_c
FSetUnion_Inter_l FSetUnion_Inter_l_c FSetUnion_Inter_r FSetUnion_Inter_r
FSetUnion_M0_s FSetUnion_M0_s_c FSetUnion_assoc FSetUnion_assoc_c FSetUnion_comm
FSetUnion_comm_c FSetUnion_idempotent FSetUnion_idempotent FSetUnion_s_M0
FSetUnion_s_M0_c FSet_Dom FSet_ext FSet_ext_c FSubset_antisym FSubset_antisym_c
FSubset_refl FSubset_trans Find Finite_downward_closed Finite_subset_has_lub
Fix_F_eq Fix_F_inv ForAll_coind
GP_finite GP_infinite G_aux Generalized_induction_on_finite_sets
Hd
INR_IZR_INZ INR_eq INR_eq_INR2 INR_fact_neq_0 INR_le INR_lt INR_lt_1 INR_pos IZN
IZR_ge IZR_le IZR_lt IfProp_false IfProp_or IfProp_sum IfProp_true Iffalse_inv
Iftrue_inv Im_add Im_def Im_inv Image_set_continuous Image_set_continuous'
InR_INV InR_app_or InR_cons_inv InR_or_app In_Image_elim In_In_spec In_dec
Included_Add Included_Empty Included_Strict_Included Inclusion_is_an_order
Inclusion_is_transitive Ind_proof Index Index_p Inhabited_Setminus Inhabited_add
Inhabited_not_empty Int_part_INR Integers_has_no_ub Integers_infinite
Intersection_commutative Intersection_decreases_l Intersection_decreases_r