coq.txt

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

Intersection_inv Intersection_is_Glb Intersection_maximal
Intersection_preserves_finite Is_power_correct Is_power_or Is_true_eq_left
Is_true_eq_right Is_true_eq_true Is_true_eq_true2 Isnil_dec Isnil_nil Item
JMeq_eq_ind JMeq_eq_ind_r JMeq_eq_rec JMeq_eq_rec_r JMeq_sym JMeq_trans
K_dec K_dec_set
L1 Lemma1 Length Length_l_pf
M1_semantics_1 M1_semantics_2 M2_eqmap_1 M2_eqmap_2 Map2_semantics_1
Map2_semantics_1_eq Map2_semantics_2 Map2_semantics_2_eq Map2_semantics_3
Map2_semantics_3_eq MapCard_Dom MapCard_Dom_Put_behind MapCard_M0 MapCard_M1
MapCard_Put1_equals_2 MapCard_Put_1 MapCard_Put_1_conv MapCard_Put_2
MapCard_Put_2_conv MapCard_Put_behind_Put MapCard_Put_behind_sum MapCard_Put_lb
MapCard_Put_sum MapCard_Put_ub MapCard_Remove_1 MapCard_Remove_1_conv
MapCard_Remove_2 MapCard_Remove_2_conv MapCard_Remove_lb MapCard_Remove_sum
MapCard_Remove_ub MapCard_as_Fold MapCard_as_Fold_1 MapCard_as_length
MapCard_ext MapCard_is_O MapCard_is_Sn MapCard_is_not_O MapCard_is_one
MapCard_is_one_unique MapCard_makeM2 MapCollect_as_Fold MapCollect_canon
MapDelta_RestrTo_disjoint MapDelta_RestrTo_disjoint_2 MapDelta_as_DomRestrBy
MapDelta_as_DomRestrBy_2 MapDelta_as_DomRestrBy_2_c MapDelta_as_DomRestrBy_c
MapDelta_as_Merge MapDelta_as_Merge_c MapDelta_canon MapDelta_disjoint
MapDelta_disjoint_c MapDelta_empty_m MapDelta_empty_m_1 MapDelta_ext
MapDelta_ext_l MapDelta_ext_r MapDelta_m_empty MapDelta_m_empty_1
MapDelta_nilpotent MapDelta_nilpotent_c MapDelta_semantics MapDelta_semantics_1
MapDelta_semantics_1_1 MapDelta_semantics_2 MapDelta_semantics_2_1
MapDelta_semantics_2_2 MapDelta_semantics_3 MapDelta_semantics_3_1
MapDelta_semantics_comm MapDelta_sym MapDelta_sym_c MapDisjoint_1_imp
MapDisjoint_2_imp MapDisjoint_M1_conv_l MapDisjoint_M1_conv_r MapDisjoint_M1_l
MapDisjoint_M1_r MapDisjoint_M2 MapDisjoint_M2_l MapDisjoint_M2_r
MapDisjoint_empty MapDisjoint_empty_c MapDisjoint_ext MapDisjoint_imp_1
MapDisjoint_imp_2 MapDisjoint_sym MapDomRestrBy_By MapDomRestrBy_By_c
MapDomRestrBy_By_comm MapDomRestrBy_By_comm_c MapDomRestrBy_Card_lb
MapDomRestrBy_Card_ub_l MapDomRestrBy_Dom MapDomRestrBy_Dom_c MapDomRestrBy_To
MapDomRestrBy_To_c MapDomRestrBy_To_comm MapDomRestrBy_To_comm_c
MapDomRestrBy_canon MapDomRestrBy_empty_m MapDomRestrBy_empty_m_1
MapDomRestrBy_ext MapDomRestrBy_ext_l MapDomRestrBy_ext_r MapDomRestrBy_m_empty
MapDomRestrBy_m_empty_1 MapDomRestrBy_m_m MapDomRestrBy_m_m_1
MapDomRestrBy_semantics MapDomRestrTo_By MapDomRestrTo_By_c
MapDomRestrTo_By_comm MapDomRestrTo_By_comm_c MapDomRestrTo_Card_ub_l
MapDomRestrTo_Card_ub_r MapDomRestrTo_Dom MapDomRestrTo_Dom_c
MapDomRestrTo_To_comm MapDomRestrTo_To_comm_c MapDomRestrTo_assoc
MapDomRestrTo_assoc_c MapDomRestrTo_canon MapDomRestrTo_empty_m
MapDomRestrTo_empty_m_1 MapDomRestrTo_ext MapDomRestrTo_ext_l
MapDomRestrTo_ext_r MapDomRestrTo_idempotent MapDomRestrTo_idempotent_c
MapDomRestrTo_m_empty MapDomRestrTo_m_empty_1 MapDomRestrTo_semantics
MapDomRestr_disjoint MapDom_Dom MapDom_Split_1 MapDom_Split_1_c MapDom_Split_2
MapDom_Split_2_c MapDom_Split_3 MapDom_Split_3_c MapDom_canon MapDom_semantics_1
MapDom_semantics_2 MapDom_semantics_3 MapDom_semantics_4 MapEmptyp_complete
MapEmptyp_correct MapFold1_as_Fold MapFold1_as_Fold_1 MapFold1_ext MapFold_M1
MapFold_Merge_disjoint MapFold_Merge_disjoint_1 MapFold_Put_behind_disjoint
MapFold_Put_behind_disjoint_2 MapFold_Put_disjoint MapFold_Put_disjoint_1
MapFold_Put_disjoint_2 MapFold_as_fold MapFold_as_fold_1 MapFold_canon
MapFold_canon_1 MapFold_distr_l MapFold_distr_r MapFold_distr_r_1 MapFold_empty
MapFold_ext MapFold_ext_f MapFold_ext_f_1 MapFold_orb MapFold_orb_1
MapFold_state_stateless MapFold_state_stateless_1 MapGet_M2_bit_0
MapGet_M2_bit_0_0 MapGet_M2_bit_0_1 MapGet_M2_bit_0_2 MapGet_M2_bit_0_if
MapGet_M2_both_NONE MapGet_if_commute MapGet_if_same MapMerge_Card_disjoint
MapMerge_Card_lb_l MapMerge_Card_lb_r MapMerge_Card_ub MapMerge_DomRestrBy
MapMerge_DomRestrBy_c MapMerge_DomRestrTo MapMerge_DomRestrTo_c
MapMerge_RestrTo_l MapMerge_RestrTo_l_c MapMerge_Restr_Card MapMerge_assoc
MapMerge_assoc_c MapMerge_canon MapMerge_disjoint MapMerge_disjoint_Card
MapMerge_empty_l MapMerge_empty_m MapMerge_empty_m_1 MapMerge_empty_m_c
MapMerge_empty_r MapMerge_ext MapMerge_ext_l MapMerge_ext_r MapMerge_idempotent
MapMerge_idempotent_c MapMerge_m_empty MapMerge_m_empty_1 MapMerge_semantics
MapPut1_canon MapPut1_semantics MapPut1_semantics' MapPut1_semantics_1
MapPut1_semantics_2 MapPut1_semantics_3 MapPut_as_Merge MapPut_as_Merge_c
MapPut_behind_as_Merge MapPut_behind_as_Merge_c MapPut_behind_as_before
MapPut_behind_as_before_1 MapPut_behind_canon MapPut_behind_ext
MapPut_behind_new MapPut_behind_semantics MapPut_behind_semantics_3_1
MapPut_canon MapPut_ext MapPut_semantics MapPut_semantics_1 MapPut_semantics_2
MapPut_semantics_2_1 MapPut_semantics_2_2 MapPut_semantics_3_1
MapRemove_as_RestrBy MapRemove_as_RestrBy_c MapRemove_canon MapRemove_ext
MapRemove_semantics MapSingleton_semantics MapSplit_Card MapSubset_1_Dom
MapSubset_1_imp MapSubset_2_imp MapSubset_Card_le MapSubset_Disjoint
MapSubset_Disjoint_l MapSubset_Disjoint_r MapSubset_DomRestrBy_l
MapSubset_DomRestrBy_mono MapSubset_DomRestrTo_l MapSubset_DomRestrTo_mono
MapSubset_DomRestrTo_r MapSubset_Dom_1 MapSubset_Dom_2 MapSubset_Merge_l
MapSubset_Merge_mono MapSubset_Merge_r MapSubset_Put MapSubset_Put_behind
MapSubset_Put_behind_mono MapSubset_Put_mono MapSubset_Remove
MapSubset_Remove_mono MapSubset_antisym MapSubset_antisym_c MapSubset_c_1
MapSubset_c_2 MapSubset_card_eq MapSubset_card_eq_1 MapSubset_ext
MapSubset_imp_1 MapSubset_imp_2 MapSubset_refl MapSubset_trans
MapSweep_semantics_1 MapSweep_semantics_1_1 MapSweep_semantics_2
MapSweep_semantics_2_1 MapSweep_semantics_2_2 MapSweep_semantics_3
MapSweep_semantics_3_1 MapSweep_semantics_4 MapSweep_semantics_4_1
Map_M0_disjoint Map_disjoint_M0 Map_of_alist_canon Map_of_alist_of_Map
Map_of_alist_of_Map_c Map_of_alist_semantics
NEG_add NEG_lt_ZERO NEG_xI NEG_xO NNPP
Noetherian_contains_Noetherian Non_disjoint_union Non_disjoint_union'
Noone_in_empty Nth
OMEGA1 OMEGA10 OMEGA11 OMEGA12 OMEGA13 OMEGA14 OMEGA15 OMEGA16 OMEGA17 OMEGA18
OMEGA19 OMEGA2 OMEGA20 OMEGA3 OMEGA4 OMEGA5 OMEGA6 OMEGA7 OMEGA8 OMEGA9 O_S
O_or_S
PI2_RGT_0 PI2_Rlt_PI PI4_RGT_0 PI4_RLT_PI2 PI6_RGT_0 PI6_RLT_PI2 PI_neq0 POS_add
POS_gt_ZERO POS_xI POS_xO Pigeonhole Pigeonhole_bis Pigeonhole_principle
Pigeonhole_ter Pow_Rabsolu Pow_x_infinity Power_monotonic Power_set_Inhabited
R0_fp_O R1_sqrt2_neq_0 RTheory R_dist_eq R_dist_plus R_dist_pos R_dist_refl
R_dist_sym R_dist_tri Rabsolu_R0 Rabsolu_R1 Rabsolu_Rabsolu Rabsolu_Rinv
Rabsolu_Ropp Rabsolu_Zabs Rabsolu_def1 Rabsolu_def2 Rabsolu_left Rabsolu_left1
Rabsolu_minus_sym Rabsolu_mult Rabsolu_no_R0 Rabsolu_pos Rabsolu_pos_eq
Rabsolu_pos_lt Rabsolu_right Rabsolu_triang Rabsolu_triang_inv Req_EM
Rge_RO_Ropp Rge_Ropp Rge_ge_eq Rge_gt_trans Rge_le Rge_minus Rge_monotony
Rge_plus_plus_r Rge_r_plus_plus Rge_trans Rgt_2PI_0 Rgt_2_0 Rgt_3PI2_0 Rgt_3_0
Rgt_RO_Ropp Rgt_Ropp Rgt_RoppO Rgt_ge Rgt_ge_trans Rgt_minus Rgt_not_eq
Rgt_not_le Rgt_plus_plus_r Rgt_r_plus_plus Rgt_trans Rinv_R1 Rinv_Rinv
Rinv_Rmult Rinv_Rmult_simpl Rinv_l_sym Rinv_lt Rinv_neq_R0 Rinv_pow Rinv_r
Rinv_r_simpl_l Rinv_r_simpl_m Rinv_r_simpl_r Rinv_r_sym Rle_RO_Ropp Rle_Rabsolu
Rle_Rmult_comp Rle_Ropp Rle_Ropp1 Rle_anti_compatibility Rle_anti_monotony
Rle_antisym Rle_compatibility Rle_compatibility_r Rle_ge Rle_le_eq Rle_lt_trans
Rle_minus Rle_monotony Rle_monotony_contra Rle_monotony_r Rle_not Rle_not_lt
Rle_or_lt Rle_sym Rle_sym1 Rle_sym2 Rle_trans Rlt_3PI2_2PI Rlt_PI_3PI2 Rlt_R0_R1
Rlt_RO_Ropp Rlt_Rinv Rlt_Rinv2 Rlt_Rinv_R1 Rlt_Ropp Rlt_Ropp1 Rlt_RoppO
Rlt_anti_compatibility Rlt_anti_monotony Rlt_antirefl Rlt_compatibility_r
Rlt_eps2_eps Rlt_eps4_eps Rlt_ge_not Rlt_le Rlt_le_not Rlt_le_trans Rlt_minus
Rlt_monotony_contra Rlt_monotony_r Rlt_monotony_rev Rlt_not_eq Rlt_not_ge
Rlt_pow Rlt_pow_R1 Rlt_r_plus_R1 Rlt_r_r_plus_R1 Rlt_rew Rlt_sqrt2_0 Rlt_sqrt3_0
Rlt_sym RmaxAbs RmaxLess1 RmaxLess2 RmaxRmult RmaxSym Rmax_Rle
Rmax_stable_in_negreal Rmin_Rgt Rmin_Rgt_l Rmin_Rgt_r Rmin_l Rmin_r
Rmin_stable_in_posreal Rminus_Int_part1 Rminus_Int_part2 Rminus_Ropp
Rminus_distr Rminus_eq Rminus_eq_contra Rminus_eq_right Rminus_fp1 Rminus_fp2
Rminus_le Rminus_lt Rminus_not_eq Rminus_not_eq_right Rmult_1r Rmult_Ol Rmult_Or
Rmult_Rplus_distrl Rmult_gt Rmult_le_pos Rmult_lt Rmult_lt2 Rmult_lt_0
Rmult_lt_pos Rmult_mult_r Rmult_ne Ropp_O Ropp_Rinv Ropp_Rle Ropp_Rlt Ropp_Ropp
Ropp_Ropp_IZR Ropp_distr1 Ropp_distr2 Ropp_distr3 Ropp_mul1 Ropp_mul2 Ropp_mul3
Ropp_neq Rplus_Or Rplus_Rminus Rplus_Ropp Rplus_Ropp_l Rplus_Rsr_eq_R0
Rplus_Rsr_eq_R0_l Rplus_contains_R Rplus_eq_R0 Rplus_eq_R0_l Rplus_le
Rplus_le_lt_lt Rplus_lt Rplus_lt_le_lt Rplus_ne Rplus_ne_i Rplus_plus_r Rsqr_1
Rsqr_O Rsqr_abs Rsqr_derivable Rsqr_derivable_pt Rsqr_derive Rsqr_div Rsqr_eq
Rsqr_eq_0 Rsqr_eq_abs_0 Rsqr_eq_asb_1 Rsqr_gt_0_0 Rsqr_incr_0 Rsqr_incr_0_var
Rsqr_incr_1 Rsqr_incrst_0 Rsqr_incrst_1 Rsqr_inj Rsqr_inv Rsqr_le_abs_0
Rsqr_le_abs_1 Rsqr_lt_abs_0 Rsqr_lt_abs_1 Rsqr_minus Rsqr_minus_plus Rsqr_neg
Rsqr_neg_minus Rsqr_neg_pos_le_0 Rsqr_neg_pos_le_1 Rsqr_plus Rsqr_plus_minus
Rsqr_pos_lt Rsqr_r_R0 Rsqr_sin_cos_d_one Rsqr_sol_eq_0_0 Rsqr_sol_eq_0_1
Rsqr_sqrt Rsqr_times Rstar'_R Rstar'_Rstar Rstar'_reflexive RstarRplus_RRstar
Rstar_R Rstar_Rstar' Rstar_cases Rstar_coherence Rstar_contains_R
Rstar_contains_Rplus Rstar_equiv_Rstar1 Rstar_imp_coherent Rstar_reflexive
Rstar_reflexive Rstar_transitive Rstar_transitive Rsym_imp_Rstarsym
Rsym_imp_notRsym
SIN SIN_bound SUPERIEUR_POS S_INR S_O_plus_INR S_pred Setminus_intro
Simplify_add Singleton_atomic Singleton_intro Singleton_inv Singleton_is_finite
Sstar_contains_Rstar Str_nth_plus Str_nth_tl_plus Strict_Included_intro
Strict_Included_inv Strict_Included_strict Strict_Rel_Transitive
Strict_Rel_Transitive_with_Rel Strict_Rel_Transitive_with_Rel_left
Strict_Rel_is_Strict_Included Strict_inclusion_is_transitive
Strict_inclusion_is_transitive_with_inclusion
Strict_inclusion_is_transitive_with_inclusion_left
Strict_super_set_contains_new_element Strong_confluence Strong_confluence_direct
Sub_Add_new Subtract_intro Subtract_inv
Tl Triple_as_Couple Triple_as_Couple_Singleton Triple_as_union Try_find
US USH Un_bound_imp Un_cv_crit Un_in_EUn Uncons Union_absorbs Union_add
Union_associative Union_commutative Union_idempotent Union_increases_l
Union_increases_r Union_inv Union_is_Lub Union_minimal Union_preserves_Finite
ZC1 ZC2 ZC3 ZC4 ZERO_le_N_digits ZERO_le_POS ZERO_le_inj ZL0 ZL1 ZL10 ZL11 ZL12
ZL12bis ZL13 ZL14 ZL15 ZL16 ZL17 ZL2 ZL3 ZL4 ZL4_inf ZL5 ZL6 ZL7 ZL8 ZLII ZLIS
ZLSI ZLSS ZS ZSH Z_R_minus Z_div_POS_ge0 Z_div_ge Z_div_ge0 Z_div_lt Z_div_mod
Z_div_mod_POS Z_div_mod_eq Z_div_plus Z_div_same Z_eq_dec Z_eq_mult Z_ge_dec
Z_ge_lt_dec Z_gt_dec Z_gt_le_dec Z_le_dec Z_le_gt_dec Z_le_lt_eq_dec
Z_lt_abs_induction Z_lt_abs_rec Z_lt_dec Z_lt_ge_dec Z_lt_induction Z_lt_rec
Z_mod_lt Z_mod_plus Z_mod_same Z_modulo_2 Z_mult_div_ge Z_zerop Zabs_Zsgn
Zabs_dec Zabs_eq Zabs_non_eq Zabs_pos Zcase_sign Zcompare_ANTISYM Zcompare_EGAL
Zcompare_Zmult_compatible Zcompare_Zmult_left Zcompare_Zmult_right Zcompare_Zopp
Zcompare_Zplus_compatible Zcompare_Zplus_compatible2 Zcompare_egal_dec
Zcompare_elim Zcompare_eq_case Zcompare_et_un Zcompare_n_S Zcompare_rec
Zcompare_trans_SUPERIEUR Zcompare_x_x Zdiv_eucl_exist Zdiv_eucl_extended
Zdiv_rest_correct Zdiv_rest_correct1 Zdiv_rest_correct2 Zegal_left Zeq_S
Zeq_Zminus Zeq_add_S Zeq_plus_swap Zero_left Zero_mult_left Zero_mult_right
Zero_right Zeven_dec Zeven_div2 Zeven_not_Zodd Zeven_odd_dec Zge_Zcompare
Zge_Zmult_pos_compat Zge_Zmult_pos_left Zge_Zmult_pos_right Zge_cases Zge_iff_le
Zge_is_le_bool Zge_le Zge_left Zge_mult_simpl Zge_trans Zgt0_le_pred Zgt_S
Zgt_S_le Zgt_S_n Zgt_Sn_n Zgt_ZERO_mult Zgt_Zcompare Zgt_Zmult_left
Zgt_Zmult_right Zgt_antirefl Zgt_cases Zgt_iff_lt Zgt_is_le_bool Zgt_le_S
Zgt_le_trans Zgt_left Zgt_left_gt Zgt_left_rev Zgt_lt Zgt_mult_simpl Zgt_n_S
Zgt_not_le Zgt_not_sym Zgt_pred Zgt_reg_l Zgt_reg_r Zgt_square_simpl Zgt_trans
Zgt_trans_S Zle_S_gt Zle_S_n Zle_Sn_n Zle_ZERO_mult Zle_Zcompare
Zle_Zmult_pos_left Zle_Zmult_pos_right Zle_Zmult_right Zle_Zmult_right2
Zle_antisym Zle_bool_antisym Zle_bool_imp_le Zle_bool_plus_mono Zle_bool_refl
Zle_bool_total Zle_bool_trans Zle_cases Zle_ge Zle_gt_S Zle_gt_trans
Zle_imp_le_bool Zle_is_le_bool Zle_le_S Zle_left Zle_left_rev Zle_lt_n_Sm
Zle_lt_or_eq Zle_lt_reg Zle_lt_trans Zle_min_l Zle_min_r Zle_mult
Zle_mult_approx Zle_mult_simpl Zle_n Zle_n_S Zle_n_Sn Zle_not_gt Zle_not_lt
Zle_or_lt Zle_plus_minus Zle_plus_plus Zle_plus_swap Zle_pred_n Zle_refl
Zle_reg_l Zle_reg_r Zle_trans Zle_trans_S Zlt_O_minus_lt Zlt_S Zlt_S_n
Zlt_ZERO_pred_le_ZERO Zlt_Zcompare Zlt_Zmult_left Zlt_Zmult_right
Zlt_Zmult_right2 Zlt_Zplus Zlt_cases Zlt_gt Zlt_is_le_bool Zlt_le_S Zlt_le_reg
Zlt_le_trans Zlt_le_weak Zlt_left Zlt_left_lt Zlt_left_rev Zlt_lt_double
Zlt_minus Zlt_n_S Zlt_n_Sm_le Zlt_n_Sn Zlt_n_n Zlt_not_eq Zlt_not_le Zlt_not_sym
Zlt_plus_swap Zlt_pred Zlt_pred_n_n Zlt_reg_l Zlt_reg_r Zlt_trans Zmin_SS
Zmin_case Zmin_n_n Zmin_or Zmin_plus Zminus_Sn_m Zminus_Zeq
Zminus_Zplus_compatible Zminus_n_O Zminus_n_n Zminus_plus Zminus_plus_simpl
Zmult_1_n Zmult_Sm_n Zmult_Zminus_distr_l Zmult_Zminus_distr_r Zmult_Zopp_Zopp
Zmult_Zopp_left Zmult_assoc Zmult_assoc_l Zmult_assoc_r Zmult_eq Zmult_gt
Zmult_le Zmult_le_approx Zmult_lt Zmult_minus_distr Zmult_n_1 Zmult_n_O
Zmult_n_Sm Zmult_one Zmult_permute Zmult_plus_distr_l Zmult_plus_distr_r
Zmult_reg_left Zmult_reg_right Zmult_sym Zmult_zero Zn_Sn Zne_left Znot_eq_S
Zodd_dec Zodd_div2 Zodd_not_Zeven Zone_min_pos Zone_pos Zopp_NEG Zopp_Zmult
Zopp_Zmult_l Zopp_Zmult_r Zopp_Zopp Zopp_Zplus Zopp_intro Zopp_one Zplus_S_n
Zplus_Snm_nSm Zplus_assoc Zplus_assoc_l Zplus_assoc_r Zplus_inverse_l
Zplus_inverse_r Zplus_minus Zplus_n_O Zplus_n_Sm Zplus_permute Zplus_simpl
Zplus_sym Zplus_unit_left Zplus_unit_right Zpower_NR0 Zpower_exp
Zpower_nat_is_exp Zpower_nat_powerRZ Zpower_nat_powerRZ_absolu Zpower_pos_is_exp
Zpower_pos_nat Zpred_Sn Zred_factor0 Zred_factor1 Zred_factor2 Zred_factor3
Zred_factor4 Zred_factor5 Zred_factor6 Zs_pred Zsgn_Zabs Zsimpl_gt_plus_l
Zsimpl_gt_plus_r Zsimpl_le_plus_l Zsimpl_le_plus_r Zsimpl_lt_plus_l
Zsimpl_lt_plus_r Zsimpl_plus_l