coq.txt

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

xH xI xO
Acc_intro
Bag Bottom_definition
Charac Couple_l Couple_r
Definition_of_Complete Definition_of_Conditionally_complete
Definition_of_Directed Definition_of_PER Definition_of_Power_set
Definition_of_covers Definition_of_equivalence Definition_of_order
Definition_of_preorder Defn_of_Approximant Disjoint_intro
EGAL Empty_is_finite
Full_intro Further
Glb_definition
Here
I INFERIEUR IT Iffalse Iftrue Im_intro In_singleton Inhabited_intro
Integers_defn Intersection_intro
JMeq_refl
Lower_Bound_definition Lt_hd Lt_nil Lt_tl Lub_definition
M0 M0_canon M1 M1_canon M2 M2_canon
NEG NONE None Nul
O
POS Pos
Rplus_0 Rplus_n Rstar1_0 Rstar1_1 Rstar1_n Rstar_0 Rstar_n
S SOME SUPERIEUR Some
Totally_ordered_definition Tree_Leaf Tree_Node Triple_l Triple_m Triple_r
Union_introl Union_intror Union_is_finite Upper_Bound_definition
ZERO Zdiv_rest_proof
/C6"Axioms"
add_0_x add_Sx_y add_assoc_l add_eq_compat add_sym arc_sin_cos archimed
bar
classic complet cos cos_0 cos_bound cos_minus cos_plus
deriv_sin deriv_sqrt derive_increasing_interv_ax derive_pt derive_pt_def
eqN eq_not_neq eq_rec_eq eq_refl eq_sym eq_trans
fct_eq foo
ge_not_lt gt_not_le
le_lt_or_eq lt lt_S_compat lt_add_compat_l lt_anti_refl lt_eq_compat lt_or_eq_le
lt_trans lt_x_Sx lt_x_Sy_le
neq_not_neq_trans neq_sym nonneg_derivative_1 not_le_gt not_lt_ge
one
positive_derivative
sigma sin sin_PI2 sin_bound sin_eq_0 sin_lb_gt_0 sin_minus sin_plus sqrt
total_order_T
up
zero
Extensionality_Ensembles
IAF
JMeq_eq
List_Dom
My_special_variable My_special_variable0 My_special_variable1
NRplus
PI PI_RGT_0
R0 R1 R1_neq_R0 Rinv Rinv_l Rlt Rlt_antisym Rlt_compatibility Rlt_monotony
Rlt_trans Rmult Rmult_1l Rmult_Rplus_distr Rmult_assoc Rmult_sym Ropp
Rplus_Ol Rplus_Ropp_r Rplus_assoc Rplus_sym
S_0_1 S_eq_compat
/C7"Modules"
auxiliary
fast_integer
zarith_aux
Adalloc AddProps Addec Addr Adist Allmaps Arith Axioms
Berardi Between Bool BoolEq
Classical Classical_Pred_Set Classical_Pred_Type Classical_Prop Classical_Type
Classical_sets Compare_dec Constructive_sets Cpo
Datatypes DatatypesSyntax DecBool Decidable Definitions DiscrAxioms DiscrProps
Disjoint_Union Div Div2
Ensembles EqAxioms EqNat EqParams Eqdep Eqdep_dec Euclid Even
Finite_sets Finite_sets_facts Fset
GeAxioms GeProps Gt GtAxioms GtProps
Heap
Image Inclusion Infinite_sets Inverse_Image
Le
LeAxioms LeProps Lexicographic_Exponentiation Lexicographic_Product List ListSet
Logic LogicSyntax Logic_Type Logic_TypeSyntax Lsort Lt LtProps
Mapaxioms Mapc Mapcanon Mapcard Mapfold Mapiter Maplists Mapsubset Max Min
Minus Mult Multiset
NSyntax NeqAxioms NeqDef NeqParams NeqProps Newman
Operators_Properties OppAxioms OppProps
Params Partial_Order Peano Peano_dec Permut Permutation Plus PolyList
PolyListSyntax Powerset Powerset_Classical_facts Powerset_facts Prelude
R_Ifp R_sqr Ranalysis Raxioms Rbase Rbasic_fun Rdefinitions Rderiv Reals
Relation_Definitions Relation_Operators Relations Relations_1 Relations_1_facts
Relations_2 Relations_2_facts Relations_3 Relations_3_facts Rfunctions Rgeom
Rlimit Rseries Rsigma Rsyntax Rtrigo Rtrigo_fun
Sorting Specif SpecifSyntax Streams SubProps
Sumbool
TheoryList Transitive_Closure TypeSyntax
Uniset
Well_Ordering Wellfounded Wf Wf_Z Wf_nat
ZArith ZArith_dec Zcomplements Zerob Zhints Zlogarithm Zmisc Zsyntax
/C8"Operators"
|
: := ::
= =>
> >>
<> << <-
->
\/
// /\
;
~
#
*
,
?
@
/
(
)
[
]
.
_PI2_RLT_0
aapp_length  absolu_lt  absoption_andb  absoption_orb  absurd  absurd_set
acc_A_B_lexprod  acc_A_sum  acc_B_sum  acc_app  ad_alloc_opt_allocates
ad_alloc_opt_allocates_1  ad_alloc_opt_optimal  ad_alloc_opt_optimal_1
ad_bit_0_0_not_double_plus_un  ad_bit_0_1_not_double  ad_bit_0_correct
ad_bit_0_gt  ad_bit_0_less  ad_bit_0_neq  ad_comp_double_inj
ad_comp_double_monotonic  ad_comp_double_plus_un_inj
ad_comp_double_plus_un_monotonic  ad_comp_monotonic  ad_div_2_correct
ad_div_2_double  ad_div_2_double_plus_un  ad_div_bit_eq  ad_div_bit_neq
ad_div_eq  ad_div_neq  ad_double_bit_0  ad_double_div_2  ad_double_inj
ad_double_monotonic  ad_double_or_double_plus_un  ad_double_plus_un_bit_0
ad_double_plus_un_div_2  ad_double_plus_un_inj  ad_double_plus_un_monotonic
ad_eq_comm  ad_eq_complete  ad_eq_correct  ad_faithful  ad_faithful_1
ad_faithful_2  ad_faithful_3  ad_faithful_4  ad_in_elems_in_list  ad_in_list_app
ad_in_list_app_1  ad_in_list_forms_circuit  ad_in_list_l
ad_in_list_of_dom_in_dom  ad_in_list_r  ad_in_list_rev  ad_ind_double
ad_le_antisym  ad_le_double_mono  ad_le_double_mono_conv
ad_le_double_plus_un_mono  ad_le_double_plus_un_mono_conv  ad_le_lt_trans
ad_le_refl  ad_le_trans  ad_less_def_1  ad_less_def_2  ad_less_def_3
ad_less_def_4  ad_less_not_refl  ad_less_total  ad_less_trans  ad_less_z
ad_list_Elems  ad_list_app_length  ad_list_app_rev  ad_list_card
ad_list_has_circuit_stutters  ad_list_not_stutters_card
ad_list_not_stutters_card_conv  ad_list_of_dom_Dom  ad_list_of_dom_Dom_1
ad_list_of_dom_card  ad_list_of_dom_card_1  ad_list_of_dom_not_stutters
ad_list_rev_length  ad_list_stutters_app_conv_l  ad_list_stutters_app_conv_r
ad_list_stutters_app_l  ad_list_stutters_app_r  ad_list_stutters_card
ad_list_stutters_card_conv  ad_list_stutters_has_circuit
ad_list_stutters_permute  ad_list_stutters_prev_conv_l
ad_list_stutters_prev_conv_r  ad_list_stutters_prev_l  ad_list_stutters_prev_r
ad_list_stutters_rev  ad_lt_double_mono  ad_lt_double_mono_conv
ad_lt_double_plus_un_mono  ad_lt_double_plus_un_mono_conv  ad_lt_le_trans
ad_lt_le_weak  ad_lt_trans  ad_min_choice  ad_min_le_1  ad_min_le_2  ad_min_le_3
ad_min_le_4  ad_min_le_5  ad_min_lt_3  ad_min_lt_4  ad_neg_bit_0  ad_neg_bit_0_1
ad_neg_bit_0_2  ad_neq  ad_not_div_2_not_double  ad_not_div_2_not_double_plus_un
ad_of_nat_of_ad  ad_pdist_comm  ad_pdist_eq_1  ad_pdist_eq_2  ad_pdist_ultra
ad_plength_first_one  ad_plength_infty  ad_plength_lb  ad_plength_one
ad_plength_ub  ad_plength_ultra  ad_plength_ultra_1  ad_plength_zeros
ad_rec_double  ad_same_bit_0  ad_sum  ad_xor_assoc  ad_xor_bit_0  ad_xor_comm
ad_xor_div_2  ad_xor_eq  ad_xor_eq_false  ad_xor_eq_true  ad_xor_neutral_left
ad_xor_neutral_right  ad_xor_nilpotent  ad_xor_sem_1  ad_xor_sem_2  ad_xor_sem_3
ad_xor_sem_4  ad_xor_sem_5  ad_xor_sem_6  ad_xor_semantics  ad_z_less_1
ad_z_less_2  add_Sx_y_swap  add_assoc  add_assoc_r  add_auto  add_one_x_S
add_soustr_1  add_soustr_2  add_soustr_xy  add_sub_one    add_un_Zs
add_verif  add_x_0  add_x_Sy  add_x_Sy_swap  add_x_one_S  add_x_x
add_x_y_z_perm  adf_xor_assoc  adf_xor_eq  alist_MapMerge_semantics
alist_MapMerge_semantics_disjoint  alist_canonical  alist_conc_sorted
alist_nth_ad_aapp_1  alist_nth_ad_aapp_2  alist_nth_ad_semantics
alist_of_Map_nth_ad  alist_of_Map_of_alist  alist_of_Map_of_alist_c
alist_of_Map_semantics  alist_of_Map_semantics_1  alist_of_Map_semantics_1_1
alist_of_Map_sorts  alist_of_Map_sorts1  alist_of_Map_sorts2
alist_of_Map_sorts_1  alist_semantics_app  alist_semantics_disjoint_comm
alist_semantics_nth_ad  alist_semantics_same_tail  alist_semantics_tail
alist_sorted_1_imp_2  alist_sorted_2_imp  alist_sorted_imp_1  alist_sorted_tail
alist_too_low  all_not_not_ex  all_not_not_ex  and_not_or  andb_assoc
andb_b_false  andb_b_true  andb_false_b  andb_false_elim  andb_false_intro1
andb_false_intro2  andb_neg_b  andb_prop  andb_prop2  andb_sym  andb_true_b
andb_true_intro  andb_true_intro2  app_ass  app_ass  app_comm_cons
app_cons_not_nil  app_eq_nil  app_eq_unit  app_inj_tail  app_length  app_nil_end
app_nil_end  approximant_can_be_any_size  approximants_grow  approximants_grow'
ass_app  ass_app  aze
base_Int_part base_fp beq_nat_refl bet_eq between_Sk_l between_in_int between_le
between_not_exists between_or_exists between_restr bij1 bij2 bij3 bool_choice
bool_eq_ind bool_eq_rec
card_Add_gen card_soustr_1 cardinalO_empty cardinal_Empty cardinal_Im_intro
cardinal_decreases cardinal_elim cardinal_finite cardinal_invert
cardinal_is_functional cardinal_unicity caseRxy case_Rabsolu cauchy_bound
classical_proof_irrelevence clos_refl_trans_ind_left clos_rst_idempotent
clos_rst_is_equiv clos_rt_clos_rst clos_rt_idempotent clos_rt_is_preorder
coherence_intro coherence_sym coherent_symmetric comm_left comm_right
compare_convert1 compare_convert_EGAL compare_convert_INFERIEUR
compare_convert_O compare_convert_SUPERIEUR compare_positive_to_nat_O
composition_derivable composition_derivable_var cong_antisymmetric_same_relation
cong_congr cong_reflexive_same_relation cong_symmetric_same_relation
cong_transitive_same_relation congr_eqT congr_idT const_continuity
const_continuous const_derivable cont_deriv contains_is_preorder convert_add
convert_add_carry convert_add_un convert_compare_EGAL convert_compare_INFERIEUR
convert_compare_SUPERIEUR convert_intro convert_xH convert_xI convert_xO cos2
cos3PI4 cos_2PI cos_2PI3 cos_2a cos_2a_cos cos_2a_sin cos_3PI2 cos_5PI4 cos_PI
cos_PI2 cos_PI3 cos_PI4 cos_PI6 cos_decr_0 cos_decr_1 cos_decreasing_0
cos_decreasing_1 cos_eq_0_0 cos_eq_0_1 cos_eq_0_2PI_0 cos_eq_0_2PI_1 cos_ge_0
cos_ge_0_3PI2 cos_gt_0 cos_incr_0 cos_incr_1 cos_increasing_0 cos_increasing_1
cos_le_0 cos_lt_0 cos_neg cos_period cos_shift cos_sin cos_sin_0 cos_sin_0_var
covers_Add covers_is_Add cvt_carry
dec_True dec_Zge dec_Zgt dec_Zle dec_Zlt dec_Zne dec_and dec_eq dec_eq_nat
dec_eq_nat dec_ge dec_gt dec_imp dec_le dec_lt dec_not dec_not_not dec_or
deg_rad demorgan1 demorgan2 demorgan3 demorgan4 deriv_Rsqr deriv_composition
deriv_const deriv_constant2 deriv_cos deriv_diff deriv_id deriv_maximum
deriv_minimum deriv_opposite deriv_prod deriv_scal deriv_sum
derivable_continuous derivable_continuous_pt derivable_derive derive_composition
derive_derivable derive_diff derive_increasing_interv
derive_increasing_interv_var derive_prod derive_pt_D_in derive_pt_cos
derive_pt_def_0 derive_pt_def_1 derive_pt_sin derive_scal derive_sum desc_end
desc_prefix desc_tail diff_Rsqr diff_comp diff_continuity diff_continuous
diff_cos diff_derivable diff_derivable_pt diff_false_true diff_id diff_plus_opp
diff_sin diff_sqrt diff_true_false discrete_nat dist_Desc_concat dist_aux
distance_refl distance_symm distr_rev div1  div2_even div2_odd