2 lines
5.8 KiB
JavaScript
2 lines
5.8 KiB
JavaScript
|
const e=Object.freeze(JSON.parse(`{"displayName":"Coq","fileTypes":["v"],"name":"coq","patterns":[{"comment":"Vernacular import keywords","match":"\\\\b(From|Require|Import|Export|Local|Global|Include)\\\\b","name":"keyword.control.import.coq"},{"comment":"Vernacular scope keywords","match":"\\\\b((Open|Close|Delimit|Undelimit|Bind)\\\\s+Scope)\\\\b","name":"keyword.control.import.coq"},{"captures":{"1":{"name":"keyword.source.coq"},"2":{"name":"entity.name.function.theorem.coq"}},"comment":"Theorem declarations","match":"\\\\b(Theorem|Lemma|Remark|Fact|Corollary|Property|Proposition|Goal)\\\\s+((\\\\p{L}|[_\\\\u00A0])(\\\\p{L}|[0-9_\\\\u00A0'])*)"},{"captures":{"1":{"name":"keyword.source.coq"},"2":{"name":"keyword.source.coq"},"3":{"name":"entity.name.assumption.coq"}},"comment":"Assumptions","match":"\\\\b(Parameters?|Axioms?|Conjectures?|Variables?|Hypothesis|Hypotheses)(\\\\s+Inline)?\\\\b\\\\s*\\\\(?\\\\s*((\\\\p{L}|[_\\\\u00A0])(\\\\p{L}|[0-9_\\\\u00A0'])*)"},{"captures":{"1":{"name":"keyword.source.coq"},"3":{"name":"entity.name.assumption.coq"}},"comment":"Context","match":"\\\\b(Context)\\\\b\\\\s*\`?\\\\s*(\\\\(|\\\\{)?\\\\s*((\\\\p{L}|[_\\\\u00A0])(\\\\p{L}|[0-9_\\\\u00A0'])*)"},{"captures":{"1":{"name":"keyword.source.coq"},"2":{"name":"keyword.source.coq"},"3":{"name":"entity.name.function.coq"}},"comment":"Definitions","match":"(\\\\b(?:Program|Local)\\\\s+)?\\\\b(Definition|Fixpoint|CoFixpoint|Function|Example|Let(?:\\\\s+Fixpoint|\\\\s+CoFixpoint)?|Instance|Equations|Equations?)\\\\s+((\\\\p{L}|[_\\\\u00A0])(\\\\p{L}|[0-9_\\\\u00A0'])*)"},{"captures":{"1":{"name":"keyword.source.coq"}},"comment":"Obligations","match":"\\\\b((Show\\\\s+)?Obligation\\\\s+Tactic|Obligations\\\\s+of|Obligation|Next\\\\s+Obligation(\\\\s+of)?|Solve\\\\s+Obligations(\\\\s+of)?|Solve\\\\s+All\\\\s+Obligations|Admit\\\\s+Obligations(\\\\s+of)?|Instance)\\\\b"},{"captures":{"1":{"name":"keyword.source.coq"},"3":{"name":"entity.name.type.coq"}},"comment":"Type declarations","match":"\\\\b(CoInductive|Inductive|Variant|Record|Structure|Class)\\\\s+(>\\\\s*)?((\\\\p{L}|[_\\\\u00A0])(\\\\p{L}|[0-9_\\\\u00A0'])*)"},{"captures":{"1":{"name":"keyword.source.coq"},"2":{"name":"entity.name.function.ltac"}},"comment":"Ltac declarations","match":"\\\\b(Ltac)\\\\s+((\\\\p{L}|[_\\\\u00A0])(\\\\p{L}|[0-9_\\\\u00A0'])*)"},{"comment":"Vernacular keywords","match":"\\\\b(Hint|Constructors|Resolve|Rewrite|Ltac|Implicit(\\\\s+Types)?|Set|Unset|Remove\\\\s+Printing|Arguments|Tactic\\\\s+Notation|Notation|Infix|Reserved\\\\s+Notation|Section|Module\\\\s+Type|Module|End|Check|Print|Eval|Search|Universe|Coercions?|Generalizable\\\\s+All|Generalizable\\\\s+Variable?|Existing\\\\s+Instance|Existing\\\\s+Class|Canonical|About|Locate|Collection|Typeclasses\\\\s+(Opaque|Transparent))\\\\b","name":"keyword.source.coq"},{"comment":"Proof keywords","match":"\\\\b(Proof|Qed|Defined|Save|Abort(\\\\s+All)?|Undo(\\\\s+To)?|Restart|Focus|Unfocus|Unfocused|Show\\\\s+Proof|Show\\\\s+Existentials|Show|Unshelve)\\\\b","name":"keyword.source.coq"},{"comment":"Vernacular Debug keywords","match":"\\\\b(Quit|Drop|Time|Redirect|Timeout|Fail)\\\\b","name":"keyword.debug.coq"},{"comment":"Admits are bad","match":"\\\\b(admit|Admitted)\\\\b","name":"invalid.illegal.admit.coq"},{"comment":"Operators","match":":|\\\\||=|<|>|\\\\*|\\\\+|-|\\\\{|\\\\}|≠|∨|∧|↔|¬|→|≤|≥","name":"keyword.operator.coq"},{"comment":"Type keywords","match":"\\\\b(forall|exists|Type|Set|Prop|nat|bool|option|list|unit|sum|prod|comparison|Empty_set)\\\\b|∀|∃","name":"support.type.coq"},{"comment":"Ltac keywords","match":"\\\\b(try|repeat|rew|progress|fresh|solve|now|first|tryif|at|once|do|only)\\\\b","name":"keyword.control.ltac"},{"comment":"Common Ltac connectors","match":"\\\\b(into|with|eqn|by|move|as|using)\\\\b","name":"keyword.control.ltac"},{"comment":"Gallina keywords","match":"\\\\b(match|lazymatch|multimatch|fun|with|return|end|let|in|if|then|else|fix|for|where|and)\\\\b|λ","name":"keyword.control.gallina"},{"comment":"Ltac builtins","match":"\\\\b(intro|intros|revert|inducti
|