coq.txt

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

/L20"Coq" Block Comment On = (* Block Comment Off = *) Escape Char = \ String Chars = " File Extensions = V COQ
/Delimiters = . ()	[]:;=`,"
/Function String = "%^{Definition^}^{Syntactic^}"
/Function String 1 = "%^{Inductive^}^{Parameter^}"
/Function String 2 = "%^{Lemma^}^{Theorem^}"
/C1"KeyWords"
arguments
else end
ident if implicit inside
of outside
then
Abort Add All Arguments AutoInline Axiom
Back Begin
Canonical Cases Cd Chapter Check Classes CoFixpoint CoInductive Coercion
Coercions Conjectures Constant Constructors Correctness
Declare Defined Definition Drop
End Eval Explicitation Export Extern Extract Extraction
Fact File Fixpoint Focus
Global Goal Grammar Graph
HintDb Hypothesis Hyps_limit
Identity If Immediate Implicit Implicits Inductive Infix Initial Inline Inspect
Language Lemma LetLibrary Load LoadPath Local Locate
ML Module Modules Morphism Mutual
NoInline
Off On Opaque Optimize
Parameter Path Paths Printing Programs Proof Pwd
Qed Quit
Read Rec Recursive Remark Remove Require Reset Resolve Restart Restore Resume
Save Scheme Script Search SearchPattern SearchRewrite Section Semi Setoid
Show Silent Structure Suspend Syntactic Syntax Synth
Table Tactic Test Theorem Time Transparent Tree
Undo Unfocus Unset
Variable Variables Verbose
Wildcard Write
/C2"Tactics"
after
in
macros
pattern
tactic tactics
until using
with
Abstract Absurd Apply Assert Assumption Auto AutoRewrite
Binding
Case CaseEqk Cbv Change Clear ClearBody Compare Compute Constructor
Contradiction Conversion Cut CutRewrite
Decide Decompose Dependent Derive Destruct DiscrR Discriminate Do Double
EApply EAuto Elim ElimCompare ElimType Equality Exact Exists
Fail Field First Fold Fourier
Generalize
Hint  Hints Hnf
Idtac Induction Injection Intro Intros Intuition Inversion Inversion_clear
Isrealint
LApply Lazy Left LetTac
Move
NewDestruct NewInduction
Omega Orelse
Pattern Pose Print Prolog
Quote
Record Red Refine Reflexivity Rename Repeat Replace Rewrite Right Ring
Setoid_replace Setoid_rewrite Simpl Simple Simplify_eq Solve Split SplitAbs
SplitAbsolu SplitRmult SqRing Sum Sup0Symmetry
Tacticals TailSimpl Tauto Transitivity Trivial Try
Unfold
/C3"IndDef"
ad and
between bool build_heap
cardinal clos_refl_sym_trans clos_refl_trans clos_trans covers
diveucl
entier eq eqT eq_dep eq_dep1 even ex ex2 exT exT2 exists
flat_spec fst_nth_spec
identityT insert_spec is_heap
le le_AsB le_WO lelistA lexprod list
mapcanon merge_lem multiset
nat natinf noetherian nth_spec
odd option or
positive prod prodT
relation
sig sig2 sigS sigS2 sigT sigT sigTT sort sum sumbool sumboolT sumor sumorT
swapprod symprod
uniset unit
Acc AllS AllS_assoc Approximant
Bottom
Complete Conditionally_complete Couple
Desc Directed Disjoint
EmptyT Empty_set Empty_set EqSt Equivalence
False Finite ForAll
Glb
IfProp Im InR In_spec Inhabited Integers Intersection
JMeq
Lower_Bound Ltl Lub
Map
Order
PER P_nth Power_set Preorder
Rplus Rstar Rstar1
Set Singleton
Totally_ordered Triple True
Union Upper_Bound
WO
Z
/C4"Definitions"
aapp absolu acons ad_alloc_opt ad_bit ad_bit_0 ad_bit_1 ad_div_2 ad_double
ad_double_plus_un ad_eq ad_eq_1 ad_in_list ad_inj ad_le ad_less ad_less_1
ad_list_of_dom ad_list_stutters ad_min ad_monotonic ad_of_nat ad_pdist
ad_plength ad_plength_1 ad_xor add_carry add_un adf_xor adhDa alist
alist_nth_ad alist_of_Map alist_semantics alist_sorted alist_sorted_1
alist_sorted_2 all allT andb andb_true_eq anil anti_convert antisymmetric app
assoc
beq_eq_not_false beq_eq_true beq_false_not_eq beq_nat beq_nat_eq bound
charac coherence coherent commut comp compare confluence confluent const
constant contains contents continue_in continuity continuity_pt convert
cos_approx cos_lb cos_term cos_ub cosd
decidable decreasing derivable derivable_pt derive dist_euc div2 div_fct
div_real_fct double double_moins_deux double_moins_un
empty_set entier_of_Z eq2eqT eqT2eq eqT_ind_r eqT_rec_r eqT_rect_r eq_S eq_dec
eq_ind_r eq_nat eq_rec_r eq_rect_r eqb eqf eqm eqmap equiv equiv_Tree error
eventually except exists_beq_eq
fact fast_OMEGA10 fast_OMEGA11 fast_OMEGA12 fast_OMEGA13 fast_OMEGA14
fast_OMEGA15 fast_OMEGA16 fast_Zmult_Zopp_left fast_Zmult_assoc_r
fast_Zmult_plus_distr fast_Zmult_sym fast_Zopp_Zmult_r fast_Zopp_Zopp
fast_Zopp_Zplus fast_Zopp_one fast_Zplus_assoc_l fast_Zplus_assoc_r
fast_Zplus_permute fast_Zplus_sym fast_Zred_factor0 fast_Zred_factor1
fast_Zred_factor2 fast_Zred_factor3 fast_Zred_factor4 fast_Zred_factor5
fast_Zred_factor6 fct_cte find fix flat_map fleche floor floor_pos fold_left
fold_right frac_part fst fstT
ge gt gtof
hd head
identityT_ind_r identityT_rec_r identityT_rect_r ifb ifdec iff implb in_FSet
in_dom in_int incl inclusion increasing index_p inf_dec infinit_sum inject_nat
injective is_lub is_upper_bound iter iter_nat iter_pos
leA_Tree le_or_le_S leb lel length lex_exp limit1_in limit_in list_contents
list_power list_prod local_confluence locally_confluent log_inf log_inf_correct1
log_inf_correct2 log_near log_sup lt lt_or_eq ltl ltof
makeM2 map max mem meq min minus minus_fct mul_factor mult mult_acc mult_fct
mult_real_fct multiplicity munion
nat_le nat_of_ad nat_po negb neq newMap ni_le ni_min no_cond notT
not_eq_false_beq nth nth_default nth_error nth_ok
opp_fct orb
p_xor permutation plat plus_acc plus_fct positive_to_nat pow powerRZ pred
prodT_curry prodT_uncurry proj1_sig proj2_sig projS1 projS2 projT1 projT2
reflexive rev
same_relation same_relation seq set set_In set_add set_diff set_fold_left
set_fold_right set_inter set_map set_mem set_power set_prod set_remove set_union
shift shift_nat shift_pos sigma_aux sin_approx sin_lb sin_term sin_ub sind snd
sndT sol_x1 sol_x2 strict_decreasing strict_increasing sub_neg sub_pos sub_un
sum_f sum_f_R0 sum_nat sum_nat_O sum_nat_f sum_nat_f_O sym_equal sym_not_equal
symmetric
tail tail_mult tail_plus tan tand times1 tl toDeg toRad trans_clos trans_equal
transitive transp try_find two_p two_power_nat two_power_pos
union
value
well_founded wof
xorb xr xt
yr yt
zerob
Acc_rec Acc_rect AllT Antisymmetric
Carrier Cauchy_crit CoInduction Compatible Complement Confluent Cons
DMerge D_in D_x Delta Delta_is_pos Descl Dgf
EUn Elems EmptyBag Emptyset Ensemble Error Ex Ex2 ExT ExT2 Exc Except
FSet FSetDelta FSetDiff FSetInter FSetUnion Fix_F Fst Fullset
IF IFProp INR INR2 INZ IZR In InR_inv Included Int_part IsSucc Is_power Is_true
Isnil
Le_AsB Length_l LexProd Lex_Exp List Locally_confluent
MapCanonicalize MapCard MapCollect MapCollect1 MapDelta MapDisjoint
MapDisjoint_1 MapDisjoint_2 MapDom MapDomRestrBy MapDomRestrTo MapEmptyp MapFold
MapFold1 MapFold1_state MapFold_state MapGet MapMerge MapPut MapPut1
MapPut_behind MapRemove MapSingleton MapSubset MapSubset_1 MapSubset_2 MapSweep
MapSweep1 MapSweep2 Map_of_alist
N_digits Nil Noetherian Not_b Nth_func
Op
Pow Power Power_set_PO ProjS1 ProjS2 Prop_S Pser
R_dist R_met Rabsolu Rdiv Reflexive Rel Relation Rge Rgt Rle Rmax Rmax_N Rmin
Rminus Rsqr Rstar'
Same_set Setminus SingletonBag Snd Str_nth Str_nth_tl Strict_Included
Strict_Rel_of Strongly_confluent Subtract SwapProd Symmetric Symprod
Transitive
Un_cv Un_growing Un_suivi_de
Value
Z_noteq_dec Z_notzerop Z_of_entier Zabs Zcompare Zdiv Zdiv2 Zdiv2_pos Zdiv_eucl
Zdiv_eucl_POS Zdiv_rest Zdiv_rest_aux Zeq_bool Zero_suivi_de Zeven Zeven_bool
Zge Zge_bool Zgt Zgt_bool Zle Zle_bool Zlt Zlt_bool Zmin Zminus Zmod Zmult
Zmult_Zplus_distr Zmult_plus_distr Zne Zneq_bool Zodd Zodd_bool Zopp Zplus
Zpower Zpower_nat Zpower_pos Zpred Zs Zsgn
/C5"Constructors"
ad_x ad_z allS_assoc_cons allS_assoc_nil allS_cons allS_nil
bet_S bet_emp
card_add card_empty conj cons cons_leA cons_sort
d_conc d_nil d_one definition_of_noetherian divex
eq_dep1_intro eq_dep_intro eqst even_O even_S exT_intro exT_intro2 ex_intro
ex_intro2 exist exist2 existS existS2 existT existTT exists_S exists_le
false flat_exist forall fst_nth_O fst_nth_S
heap_exist
inR_hd inR_tl in_hd in_tl infty inl inleft inleftT inr inright inrightT
insert_exist
le_S le_aa le_ab le_bb le_n le_sup left leftT left_lex left_sym
merge_exist
ni nil nil_is_heap nil_leA nil_sort node_is_heap nth_O nth_S nth_spec_O
nth_spec_S
odd_S or_introl or_intror
pair pairT
refl_eqT
refl_equal refl_identity refl_identityT right rightT right_lex right_sym
rst_refl rst_step rst_sym rst_trans rt_refl rt_step rt_trans
sp_noswap sp_swap sup
t_step t_trans true tt