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