static/highlight/es/languages/coq.js

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