coq top-level property

Language coq

Implementation

final coq = Language(
  id: "coq",
  refs: {},
  name: "Coq",
  keywords: {
    "keyword": [
      "_|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"
    ],
    "built_in": [
      "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"
    ]
  },
  contains: [
    QUOTE_STRING_MODE,
    Mode(
      scope: "comment",
      begin: "\\(\\*",
      end: "\\*\\)",
      contains: [
        Mode(
          scope: "doctag",
          begin: "[ ]*(?=(TODO|FIXME|NOTE|BUG|OPTIMIZE|HACK|XXX):)",
          end: "(TODO|FIXME|NOTE|BUG|OPTIMIZE|HACK|XXX):",
          excludeBegin: true,
          relevance: 0,
        ),
        Mode(
          begin:
              "[ ]+((?:I|a|is|so|us|to|at|if|in|it|on|[A-Za-z]+['](d|ve|re|ll|t|s|n)|[A-Za-z]+[-][a-z]+|[A-Za-z][a-z]{2,})[.]?[:]?([.][ ]|[ ])){3}",
        ),
      ],
    ),
    C_NUMBER_MODE,
    Mode(
      className: "type",
      excludeBegin: true,
      begin: "\\|\\s*",
      end: "\\w+",
    ),
    Mode(
      begin: "[-=]>",
    ),
  ],
);