You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
80 lines
4.3 KiB
80 lines
4.3 KiB
4 years ago
|
/*
|
||
|
|
Language: Coq
|
||
|
|
Author: Stephan Boyer <stephan@stephanboyer.com>
|
||
|
|
Category: functional
|
||
|
|
Website: https://coq.inria.fr
|
||
|
|
*/
|
||
|
|
|
||
|
|
/** @type LanguageFn */
|
||
|
|
function coq(hljs) {
|
||
|
|
return {
|
||
|
|
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: [
|
||
|
|
hljs.QUOTE_STRING_MODE,
|
||
|
|
hljs.COMMENT('\\(\\*', '\\*\\)'),
|
||
|
|
hljs.C_NUMBER_MODE,
|
||
|
|
{
|
||
|
|
className: 'type',
|
||
|
|
excludeBegin: true,
|
||
|
|
begin: '\\|\\s*',
|
||
|
|
end: '\\w+'
|
||
|
|
},
|
||
|
|
{ // relevance booster
|
||
|
|
begin: /[-=]>/
|
||
|
|
}
|
||
|
|
]
|
||
|
|
};
|
||
|
|
}
|
||
|
|
|
||
|
|
module.exports = coq;
|