ai/world
1
0
Fork 0
Code Issues Releases Activity

fix

Browse Source
This commit is contained in:
syui
2025-05-12 05:38:44 +09:00
parent dced21c3f8
commit 6d78bfa46e
8120 changed files with 1161564 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

445
book/node_modules/highlight.js/es/languages/coq.js generated vendored Normal file
View File

@ -0,0 +1,445 @@
/*
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 };