2023-10-03 11:14:36 +08:00
|
|
|
/*
|
|
|
|
|
Language: Coq
|
|
|
|
|
Author: Stephan Boyer <stephan@stephanboyer.com>
|
|
|
|
|
Category: functional
|
|
|
|
|
Website: https://coq.inria.fr
|
|
|
|
|
*/
|
|
|
|
|
|
|
|
|
|
/** @type LanguageFn */
|
|
|
|
|
function coq(hljs) {
|
|
|
|
|
const KEYWORDS = [
|
|
|
|
|
"_|0",
|
|
|
|
|
"as",
|
|
|
|
|
"at",
|
|
|
|
|
"cofix",
|
|
|
|
|
"else",
|
|
|
|
|
"end",
|
|
|
|
|
"exists",
|
|
|
|
|
"exists2",
|
|
|
|
|
"fix",
|
|
|
|
|
"for",
|
|
|
|
|
"forall",
|
|
|
|
|
"fun",
|
|
|
|
|
"if",
|
|
|
|
|
"IF",
|
|
|
|
|
"in",
|
|
|
|
|
"let",
|
|
|
|
|
"match",
|
|
|
|
|
"mod",
|
|
|
|
|
"Prop",
|
|
|
|
|
"return",
|
|
|
|
|
"Set",
|
|
|
|
|
"then",
|
|
|
|
|
"Type",
|
|
|
|
|
"using",
|
|
|
|
|
"where",
|
|
|
|
|
"with",
|
|
|
|
|
"Abort",
|
|
|
|
|
"About",
|
|
|
|
|
"Add",
|
|
|
|
|
"Admit",
|
|
|
|
|
"Admitted",
|
|
|
|
|
"All",
|
|
|
|
|
"Arguments",
|
|
|
|
|
"Assumptions",
|
|
|
|
|
"Axiom",
|
|
|
|
|
"Back",
|
|
|
|
|
"BackTo",
|
|
|
|
|
"Backtrack",
|
|
|
|
|
"Bind",
|
|
|
|
|
"Blacklist",
|
|
|
|
|
"Canonical",
|
|
|
|
|
"Cd",
|
|
|
|
|
"Check",
|
|
|
|
|
"Class",
|
|
|
|
|
"Classes",
|
|
|
|
|
"Close",
|
|
|
|
|
"Coercion",
|
|
|
|
|
"Coercions",
|
|
|
|
|
"CoFixpoint",
|
|
|
|
|
"CoInductive",
|
|
|
|
|
"Collection",
|
|
|
|
|
"Combined",
|
|
|
|
|
"Compute",
|
|
|
|
|
"Conjecture",
|
|
|
|
|
"Conjectures",
|
|
|
|
|
"Constant",
|
|
|
|
|
"constr",
|
|
|
|
|
"Constraint",
|
|
|
|
|
"Constructors",
|
|
|
|
|
"Context",
|
|
|
|
|
"Corollary",
|
|
|
|
|
"CreateHintDb",
|
|
|
|
|
"Cut",
|
|
|
|
|
"Declare",
|
|
|
|
|
"Defined",
|
|
|
|
|
"Definition",
|
|
|
|
|
"Delimit",
|
|
|
|
|
"Dependencies",
|
|
|
|
|
"Dependent",
|
|
|
|
|
"Derive",
|
|
|
|
|
"Drop",
|
|
|
|
|
"eauto",
|
|
|
|
|
"End",
|
|
|
|
|
"Equality",
|
|
|
|
|
"Eval",
|
|
|
|
|
"Example",
|
|
|
|
|
"Existential",
|
|
|
|
|
"Existentials",
|
|
|
|
|
"Existing",
|
|
|
|
|
"Export",
|
|
|
|
|
"exporting",
|
|
|
|
|
"Extern",
|
|
|
|
|
"Extract",
|
|
|
|
|
"Extraction",
|
|
|
|
|
"Fact",
|
|
|
|
|
"Field",
|
|
|
|
|
"Fields",
|
|
|
|
|
"File",
|
|
|
|
|
"Fixpoint",
|
|
|
|
|
"Focus",
|
|
|
|
|
"for",
|
|
|
|
|
"From",
|
|
|
|
|
"Function",
|
|
|
|
|
"Functional",
|
|
|
|
|
"Generalizable",
|
|
|
|
|
"Global",
|
|
|
|
|
"Goal",
|
|
|
|
|
"Grab",
|
|
|
|
|
"Grammar",
|
|
|
|
|
"Graph",
|
|
|
|
|
"Guarded",
|
|
|
|
|
"Heap",
|
|
|
|
|
"Hint",
|
|
|
|
|
"HintDb",
|
|
|
|
|
"Hints",
|
|
|
|
|
"Hypotheses",
|
|
|
|
|
"Hypothesis",
|
|
|
|
|
"ident",
|
|
|
|
|
"Identity",
|
|
|
|
|
"If",
|
|
|
|
|
"Immediate",
|
|
|
|
|
"Implicit",
|
|
|
|
|
"Import",
|
|
|
|
|
"Include",
|
|
|
|
|
"Inductive",
|
|
|
|
|
"Infix",
|
|
|
|
|
"Info",
|
|
|
|
|
"Initial",
|
|
|
|
|
"Inline",
|
|
|
|
|
"Inspect",
|
|
|
|
|
"Instance",
|
|
|
|
|
"Instances",
|
|
|
|
|
"Intro",
|
|
|
|
|
"Intros",
|
|
|
|
|
"Inversion",
|
|
|
|
|
"Inversion_clear",
|
|
|
|
|
"Language",
|
|
|
|
|
"Left",
|
|
|
|
|
"Lemma",
|
|
|
|
|
"Let",
|
|
|
|
|
"Libraries",
|
|
|
|
|
"Library",
|
|
|
|
|
"Load",
|
|
|
|
|
"LoadPath",
|
|
|
|
|
"Local",
|
|
|
|
|
"Locate",
|
|
|
|
|
"Ltac",
|
|
|
|
|
"ML",
|
|
|
|
|
"Mode",
|
|
|
|
|
"Module",
|
|
|
|
|
"Modules",
|
|
|
|
|
"Monomorphic",
|
|
|
|
|
"Morphism",
|
|
|
|
|
"Next",
|
|
|
|
|
"NoInline",
|
|
|
|
|
"Notation",
|
|
|
|
|
"Obligation",
|
|
|
|
|
"Obligations",
|
|
|
|
|
"Opaque",
|
|
|
|
|
"Open",
|
|
|
|
|
"Optimize",
|
|
|
|
|
"Options",
|
|
|
|
|
"Parameter",
|
|
|
|
|
"Parameters",
|
|
|
|
|
"Parametric",
|
|
|
|
|
"Path",
|
|
|
|
|
"Paths",
|
|
|
|
|
"pattern",
|
|
|
|
|
"Polymorphic",
|
|
|
|
|
"Preterm",
|
|
|
|
|
"Print",
|
|
|
|
|
"Printing",
|
|
|
|
|
"Program",
|
|
|
|
|
"Projections",
|
|
|
|
|
"Proof",
|
|
|
|
|
"Proposition",
|
|
|
|
|
"Pwd",
|
|
|
|
|
"Qed",
|
|
|
|
|
"Quit",
|
|
|
|
|
"Rec",
|
|
|
|
|
"Record",
|
|
|
|
|
"Recursive",
|
|
|
|
|
"Redirect",
|
|
|
|
|
"Relation",
|
|
|
|
|
"Remark",
|
|
|
|
|
"Remove",
|
|
|
|
|
"Require",
|
|
|
|
|
"Reserved",
|
|
|
|
|
"Reset",
|
|
|
|
|
"Resolve",
|
|
|
|
|
"Restart",
|
|
|
|
|
"Rewrite",
|
|
|
|
|
"Right",
|
|
|
|
|
"Ring",
|
|
|
|
|
"Rings",
|
|
|
|
|
"Save",
|
|
|
|
|
"Scheme",
|
|
|
|
|
"Scope",
|
|
|
|
|
"Scopes",
|
|
|
|
|
"Script",
|
|
|
|
|
"Search",
|
|
|
|
|
"SearchAbout",
|
|
|
|
|
"SearchHead",
|
|
|
|
|
"SearchPattern",
|
|
|
|
|
"SearchRewrite",
|
|
|
|
|
"Section",
|
|
|
|
|
"Separate",
|
|
|
|
|
"Set",
|
|
|
|
|
"Setoid",
|
|
|
|
|
"Show",
|
|
|
|
|
"Solve",
|
|
|
|
|
"Sorted",
|
|
|
|
|
"Step",
|
|
|
|
|
"Strategies",
|
|
|
|
|
"Strategy",
|
|
|
|
|
"Structure",
|
|
|
|
|
"SubClass",
|
|
|
|
|
"Table",
|
|
|
|
|
"Tables",
|
|
|
|
|
"Tactic",
|
|
|
|
|
"Term",
|
|
|
|
|
"Test",
|
|
|
|
|
"Theorem",
|
|
|
|
|
"Time",
|
|
|
|
|
"Timeout",
|
|
|
|
|
"Transparent",
|
|
|
|
|
"Type",
|
|
|
|
|
"Typeclasses",
|
|
|
|
|
"Types",
|
|
|
|
|
"Undelimit",
|
|
|
|
|
"Undo",
|
|
|
|
|
"Unfocus",
|
|
|
|
|
"Unfocused",
|
|
|
|
|
"Unfold",
|
|
|
|
|
"Universe",
|
|
|
|
|
"Universes",
|
|
|
|
|
"Unset",
|
|
|
|
|
"Unshelve",
|
|
|
|
|
"using",
|
|
|
|
|
"Variable",
|
|
|
|
|
"Variables",
|
|
|
|
|
"Variant",
|
|
|
|
|
"Verbose",
|
|
|
|
|
"Visibility",
|
|
|
|
|
"where",
|
|
|
|
|
"with"
|
|
|
|
|
];
|
|
|
|
|
const BUILT_INS = [
|
|
|
|
|
"abstract",
|
|
|
|
|
"absurd",
|
|
|
|
|
"admit",
|
|
|
|
|
"after",
|
|
|
|
|
"apply",
|
|
|
|
|
"as",
|
|
|
|
|
"assert",
|
|
|
|
|
"assumption",
|
|
|
|
|
"at",
|
|
|
|
|
"auto",
|
|
|
|
|
"autorewrite",
|
|
|
|
|
"autounfold",
|
|
|
|
|
"before",
|
|
|
|
|
"bottom",
|
|
|
|
|
"btauto",
|
|
|
|
|
"by",
|
|
|
|
|
"case",
|
|
|
|
|
"case_eq",
|
|
|
|
|
"cbn",
|
|
|
|
|
"cbv",
|
|
|
|
|
"change",
|
|
|
|
|
"classical_left",
|
|
|
|
|
"classical_right",
|
|
|
|
|
"clear",
|
|
|
|
|
"clearbody",
|
|
|
|
|
"cofix",
|
|
|
|
|
"compare",
|
|
|
|
|
"compute",
|
|
|
|
|
"congruence",
|
|
|
|
|
"constr_eq",
|
|
|
|
|
"constructor",
|
|
|
|
|
"contradict",
|
|
|
|
|
"contradiction",
|
|
|
|
|
"cut",
|
|
|
|
|
"cutrewrite",
|
|
|
|
|
"cycle",
|
|
|
|
|
"decide",
|
|
|
|
|
"decompose",
|
|
|
|
|
"dependent",
|
|
|
|
|
"destruct",
|
|
|
|
|
"destruction",
|
|
|
|
|
"dintuition",
|
|
|
|
|
"discriminate",
|
|
|
|
|
"discrR",
|
|
|
|
|
"do",
|
|
|
|
|
"double",
|
|
|
|
|
"dtauto",
|
|
|
|
|
"eapply",
|
|
|
|
|
"eassumption",
|
|
|
|
|
"eauto",
|
|
|
|
|
"ecase",
|
|
|
|
|
"econstructor",
|
|
|
|
|
"edestruct",
|
|
|
|
|
"ediscriminate",
|
|
|
|
|
"eelim",
|
|
|
|
|
"eexact",
|
|
|
|
|
"eexists",
|
|
|
|
|
"einduction",
|
|
|
|
|
"einjection",
|
|
|
|
|
"eleft",
|
|
|
|
|
"elim",
|
|
|
|
|
"elimtype",
|
|
|
|
|
"enough",
|
|
|
|
|
"equality",
|
|
|
|
|
"erewrite",
|
|
|
|
|
"eright",
|
|
|
|
|
"esimplify_eq",
|
|
|
|
|
"esplit",
|
|
|
|
|
"evar",
|
|
|
|
|
"exact",
|
|
|
|
|
"exactly_once",
|
|
|
|
|
"exfalso",
|
|
|
|
|
"exists",
|
|
|
|
|
"f_equal",
|
|
|
|
|
"fail",
|
|
|
|
|
"field",
|
|
|
|
|
"field_simplify",
|
|
|
|
|
"field_simplify_eq",
|
|
|
|
|
"first",
|
|
|
|
|
"firstorder",
|
|
|
|
|
"fix",
|
|
|
|
|
"fold",
|
|
|
|
|
"fourier",
|
|
|
|
|
"functional",
|
|
|
|
|
"generalize",
|
|
|
|
|
"generalizing",
|
|
|
|
|
"gfail",
|
|
|
|
|
"give_up",
|
|
|
|
|
"has_evar",
|
|
|
|
|
"hnf",
|
|
|
|
|
"idtac",
|
|
|
|
|
"in",
|
|
|
|
|
"induction",
|
|
|
|
|
"injection",
|
|
|
|
|
"instantiate",
|
|
|
|
|
"intro",
|
|
|
|
|
"intro_pattern",
|
|
|
|
|
"intros",
|
|
|
|
|
"intuition",
|
|
|
|
|
"inversion",
|
|
|
|
|
"inversion_clear",
|
|
|
|
|
"is_evar",
|
|
|
|
|
"is_var",
|
|
|
|
|
"lapply",
|
|
|
|
|
"lazy",
|
|
|
|
|
"left",
|
|
|
|
|
"lia",
|
|
|
|
|
"lra",
|
|
|
|
|
"move",
|
|
|
|
|
"native_compute",
|
|
|
|
|
"nia",
|
|
|
|
|
"nsatz",
|
|
|
|
|
"omega",
|
|
|
|
|
"once",
|
|
|
|
|
"pattern",
|
|
|
|
|
"pose",
|
|
|
|
|
"progress",
|
|
|
|
|
"proof",
|
|
|
|
|
"psatz",
|
|
|
|
|
"quote",
|
|
|
|
|
"record",
|
|
|
|
|
"red",
|
|
|
|
|
"refine",
|
|
|
|
|
"reflexivity",
|
|
|
|
|
"remember",
|
|
|
|
|
"rename",
|
|
|
|
|
"repeat",
|
|
|
|
|
"replace",
|
|
|
|
|
"revert",
|
|
|
|
|
"revgoals",
|
|
|
|
|
"rewrite",
|
|
|
|
|
"rewrite_strat",
|
|
|
|
|
"right",
|
|
|
|
|
"ring",
|
|
|
|
|
"ring_simplify",
|
|
|
|
|
"rtauto",
|
|
|
|
|
"set",
|
|
|
|
|
"setoid_reflexivity",
|
|
|
|
|
"setoid_replace",
|
|
|
|
|
"setoid_rewrite",
|
|
|
|
|
"setoid_symmetry",
|
|
|
|
|
"setoid_transitivity",
|
|
|
|
|
"shelve",
|
|
|
|
|
"shelve_unifiable",
|
|
|
|
|
"simpl",
|
|
|
|
|
"simple",
|
|
|
|
|
"simplify_eq",
|
|
|
|
|
"solve",
|
|
|
|
|
"specialize",
|
|
|
|
|
"split",
|
|
|
|
|
"split_Rabs",
|
|
|
|
|
"split_Rmult",
|
|
|
|
|
"stepl",
|
|
|
|
|
"stepr",
|
|
|
|
|
"subst",
|
|
|
|
|
"sum",
|
|
|
|
|
"swap",
|
|
|
|
|
"symmetry",
|
|
|
|
|
"tactic",
|
|
|
|
|
"tauto",
|
|
|
|
|
"time",
|
|
|
|
|
"timeout",
|
|
|
|
|
"top",
|
|
|
|
|
"transitivity",
|
|
|
|
|
"trivial",
|
|
|
|
|
"try",
|
|
|
|
|
"tryif",
|
|
|
|
|
"unfold",
|
|
|
|
|
"unify",
|
|
|
|
|
"until",
|
|
|
|
|
"using",
|
|
|
|
|
"vm_compute",
|
|
|
|
|
"with"
|
|
|
|
|
];
|
|
|
|
|
return {
|
|
|
|
|
name: 'Coq',
|
|
|
|
|
keywords: {
|
|
|
|
|
keyword: KEYWORDS,
|
|
|
|
|
built_in: BUILT_INS
|
|
|
|
|
},
|
|
|
|
|
contains: [
|
|
|
|
|
hljs.QUOTE_STRING_MODE,
|
|
|
|
|
hljs.COMMENT('\\(\\*', '\\*\\)'),
|
|
|
|
|
hljs.C_NUMBER_MODE,
|
|
|
|
|
{
|
|
|
|
|
className: 'type',
|
|
|
|
|
excludeBegin: true,
|
|
|
|
|
begin: '\\|\\s*',
|
|
|
|
|
end: '\\w+'
|
|
|
|
|
},
|
|
|
|
|
{ // relevance booster
|
|
|
|
|
begin: /[-=]>/ }
|
|
|
|
|
]
|
|
|
|
|
};
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
export { coq as default };
|
