static/highlight/languages/coq.js

   1 /*! `coq` grammar compiled for Highlight.js 11.11.1 */
   2   (function(){
   3     var hljsGrammar = (function () {
   4   'use strict';
   5
   6   /*
   7   Language: Coq
   8   Author: Stephan Boyer <stephan@stephanboyer.com>
   9   Category: functional
  10   Website: https://coq.inria.fr
  11   */
  12
  13   /** @type LanguageFn */
  14   function coq(hljs) {
  15     const KEYWORDS = [
  16       "_|0",
  17       "as",
  18       "at",
  19       "cofix",
  20       "else",
  21       "end",
  22       "exists",
  23       "exists2",
  24       "fix",
  25       "for",
  26       "forall",
  27       "fun",
  28       "if",
  29       "IF",
  30       "in",
  31       "let",
  32       "match",
  33       "mod",
  34       "Prop",
  35       "return",
  36       "Set",
  37       "then",
  38       "Type",
  39       "using",
  40       "where",
  41       "with",
  42       "Abort",
  43       "About",
  44       "Add",
  45       "Admit",
  46       "Admitted",
  47       "All",
  48       "Arguments",
  49       "Assumptions",
  50       "Axiom",
  51       "Back",
  52       "BackTo",
  53       "Backtrack",
  54       "Bind",
  55       "Blacklist",
  56       "Canonical",
  57       "Cd",
  58       "Check",
  59       "Class",
  60       "Classes",
  61       "Close",
  62       "Coercion",
  63       "Coercions",
  64       "CoFixpoint",
  65       "CoInductive",
  66       "Collection",
  67       "Combined",
  68       "Compute",
  69       "Conjecture",
  70       "Conjectures",
  71       "Constant",
  72       "constr",
  73       "Constraint",
  74       "Constructors",
  75       "Context",
  76       "Corollary",
  77       "CreateHintDb",
  78       "Cut",
  79       "Declare",
  80       "Defined",
  81       "Definition",
  82       "Delimit",
  83       "Dependencies",
  84       "Dependent",
  85       "Derive",
  86       "Drop",
  87       "eauto",
  88       "End",
  89       "Equality",
  90       "Eval",
  91       "Example",
  92       "Existential",
  93       "Existentials",
  94       "Existing",
  95       "Export",
  96       "exporting",
  97       "Extern",
  98       "Extract",
  99       "Extraction",
 100       "Fact",
 101       "Field",
 102       "Fields",
 103       "File",
 104       "Fixpoint",
 105       "Focus",
 106       "for",
 107       "From",
 108       "Function",
 109       "Functional",
 110       "Generalizable",
 111       "Global",
 112       "Goal",
 113       "Grab",
 114       "Grammar",
 115       "Graph",
 116       "Guarded",
 117       "Heap",
 118       "Hint",
 119       "HintDb",
 120       "Hints",
 121       "Hypotheses",
 122       "Hypothesis",
 123       "ident",
 124       "Identity",
 125       "If",
 126       "Immediate",
 127       "Implicit",
 128       "Import",
 129       "Include",
 130       "Inductive",
 131       "Infix",
 132       "Info",
 133       "Initial",
 134       "Inline",
 135       "Inspect",
 136       "Instance",
 137       "Instances",
 138       "Intro",
 139       "Intros",
 140       "Inversion",
 141       "Inversion_clear",
 142       "Language",
 143       "Left",
 144       "Lemma",
 145       "Let",
 146       "Libraries",
 147       "Library",
 148       "Load",
 149       "LoadPath",
 150       "Local",
 151       "Locate",
 152       "Ltac",
 153       "ML",
 154       "Mode",
 155       "Module",
 156       "Modules",
 157       "Monomorphic",
 158       "Morphism",
 159       "Next",
 160       "NoInline",
 161       "Notation",
 162       "Obligation",
 163       "Obligations",
 164       "Opaque",
 165       "Open",
 166       "Optimize",
 167       "Options",
 168       "Parameter",
 169       "Parameters",
 170       "Parametric",
 171       "Path",
 172       "Paths",
 173       "pattern",
 174       "Polymorphic",
 175       "Preterm",
 176       "Print",
 177       "Printing",
 178       "Program",
 179       "Projections",
 180       "Proof",
 181       "Proposition",
 182       "Pwd",
 183       "Qed",
 184       "Quit",
 185       "Rec",
 186       "Record",
 187       "Recursive",
 188       "Redirect",
 189       "Relation",
 190       "Remark",
 191       "Remove",
 192       "Require",
 193       "Reserved",
 194       "Reset",
 195       "Resolve",
 196       "Restart",
 197       "Rewrite",
 198       "Right",
 199       "Ring",
 200       "Rings",
 201       "Save",
 202       "Scheme",
 203       "Scope",
 204       "Scopes",
 205       "Script",
 206       "Search",
 207       "SearchAbout",
 208       "SearchHead",
 209       "SearchPattern",
 210       "SearchRewrite",
 211       "Section",
 212       "Separate",
 213       "Set",
 214       "Setoid",
 215       "Show",
 216       "Solve",
 217       "Sorted",
 218       "Step",
 219       "Strategies",
 220       "Strategy",
 221       "Structure",
 222       "SubClass",
 223       "Table",
 224       "Tables",
 225       "Tactic",
 226       "Term",
 227       "Test",
 228       "Theorem",
 229       "Time",
 230       "Timeout",
 231       "Transparent",
 232       "Type",
 233       "Typeclasses",
 234       "Types",
 235       "Undelimit",
 236       "Undo",
 237       "Unfocus",
 238       "Unfocused",
 239       "Unfold",
 240       "Universe",
 241       "Universes",
 242       "Unset",
 243       "Unshelve",
 244       "using",
 245       "Variable",
 246       "Variables",
 247       "Variant",
 248       "Verbose",
 249       "Visibility",
 250       "where",
 251       "with"
 252     ];
 253     const BUILT_INS = [
 254       "abstract",
 255       "absurd",
 256       "admit",
 257       "after",
 258       "apply",
 259       "as",
 260       "assert",
 261       "assumption",
 262       "at",
 263       "auto",
 264       "autorewrite",
 265       "autounfold",
 266       "before",
 267       "bottom",
 268       "btauto",
 269       "by",
 270       "case",
 271       "case_eq",
 272       "cbn",
 273       "cbv",
 274       "change",
 275       "classical_left",
 276       "classical_right",
 277       "clear",
 278       "clearbody",
 279       "cofix",
 280       "compare",
 281       "compute",
 282       "congruence",
 283       "constr_eq",
 284       "constructor",
 285       "contradict",
 286       "contradiction",
 287       "cut",
 288       "cutrewrite",
 289       "cycle",
 290       "decide",
 291       "decompose",
 292       "dependent",
 293       "destruct",
 294       "destruction",
 295       "dintuition",
 296       "discriminate",
 297       "discrR",
 298       "do",
 299       "double",
 300       "dtauto",
 301       "eapply",
 302       "eassumption",
 303       "eauto",
 304       "ecase",
 305       "econstructor",
 306       "edestruct",
 307       "ediscriminate",
 308       "eelim",
 309       "eexact",
 310       "eexists",
 311       "einduction",
 312       "einjection",
 313       "eleft",
 314       "elim",
 315       "elimtype",
 316       "enough",
 317       "equality",
 318       "erewrite",
 319       "eright",
 320       "esimplify_eq",
 321       "esplit",
 322       "evar",
 323       "exact",
 324       "exactly_once",
 325       "exfalso",
 326       "exists",
 327       "f_equal",
 328       "fail",
 329       "field",
 330       "field_simplify",
 331       "field_simplify_eq",
 332       "first",
 333       "firstorder",
 334       "fix",
 335       "fold",
 336       "fourier",
 337       "functional",
 338       "generalize",
 339       "generalizing",
 340       "gfail",
 341       "give_up",
 342       "has_evar",
 343       "hnf",
 344       "idtac",
 345       "in",
 346       "induction",
 347       "injection",
 348       "instantiate",
 349       "intro",
 350       "intro_pattern",
 351       "intros",
 352       "intuition",
 353       "inversion",
 354       "inversion_clear",
 355       "is_evar",
 356       "is_var",
 357       "lapply",
 358       "lazy",
 359       "left",
 360       "lia",
 361       "lra",
 362       "move",
 363       "native_compute",
 364       "nia",
 365       "nsatz",
 366       "omega",
 367       "once",
 368       "pattern",
 369       "pose",
 370       "progress",
 371       "proof",
 372       "psatz",
 373       "quote",
 374       "record",
 375       "red",
 376       "refine",
 377       "reflexivity",
 378       "remember",
 379       "rename",
 380       "repeat",
 381       "replace",
 382       "revert",
 383       "revgoals",
 384       "rewrite",
 385       "rewrite_strat",
 386       "right",
 387       "ring",
 388       "ring_simplify",
 389       "rtauto",
 390       "set",
 391       "setoid_reflexivity",
 392       "setoid_replace",
 393       "setoid_rewrite",
 394       "setoid_symmetry",
 395       "setoid_transitivity",
 396       "shelve",
 397       "shelve_unifiable",
 398       "simpl",
 399       "simple",
 400       "simplify_eq",
 401       "solve",
 402       "specialize",
 403       "split",
 404       "split_Rabs",
 405       "split_Rmult",
 406       "stepl",
 407       "stepr",
 408       "subst",
 409       "sum",
 410       "swap",
 411       "symmetry",
 412       "tactic",
 413       "tauto",
 414       "time",
 415       "timeout",
 416       "top",
 417       "transitivity",
 418       "trivial",
 419       "try",
 420       "tryif",
 421       "unfold",
 422       "unify",
 423       "until",
 424       "using",
 425       "vm_compute",
 426       "with"
 427     ];
 428     return {
 429       name: 'Coq',
 430       keywords: {
 431         keyword: KEYWORDS,
 432         built_in: BUILT_INS
 433       },
 434       contains: [
 435         hljs.QUOTE_STRING_MODE,
 436         hljs.COMMENT('\\(\\*', '\\*\\)'),
 437         hljs.C_NUMBER_MODE,
 438         {
 439           className: 'type',
 440           excludeBegin: true,
 441           begin: '\\|\\s*',
 442           end: '\\w+'
 443         },
 444         { // relevance booster
 445           begin: /[-=]>/ }
 446       ]
 447     };
 448   }
 449
 450   return coq;
 451
 452 })();
 453
 454     hljs.registerLanguage('coq', hljsGrammar);
 455   })();