class Rouge::Lexers::Coq
def self.classify(x)
def self.classify(x) if self.coq.include? x return Keyword elsif self.gallina.include? x return Keyword::Reserved elsif self.ltac.include? x return Keyword::Pseudo elsif self.terminators.include? x return Name::Exception elsif self.tacticals.include? x return Keyword::Pseudo else return Name::Constant end end
def self.coq
def self.coq @coq ||= Set.new %w( Definition Theorem Lemma Remark Example Fixpoint CoFixpoint Record Inductive CoInductive Corollary Goal Proof Ltac Require Import Export Module Section End Variable Context Polymorphic Monomorphic Universe Universes Variables Class Instance Global Local Include Printing Notation Infix Arguments Hint Rewrite Immediate Qed Defined Opaque Transparent Existing Compute Eval Print SearchAbout Search About Check ) end
def self.end_sentence
def self.end_sentence @end_sentence ||= Punctuation::Indicator end
def self.gallina
def self.gallina @gallina ||= Set.new %w( as fun if in let match then else return end Type Set Prop forall ) end
def self.keyopts
def self.keyopts @keyopts ||= Set.new %w( := => -> /\\ \\/ _ ; :> : ) end
def self.ltac
def self.ltac @ltac ||= Set.new %w( apply eapply auto eauto rewrite setoid_rewrite with in as at destruct split inversion injection intro intros unfold fold cbv cbn lazy subst clear symmetry transitivity etransitivity erewrite edestruct constructor econstructor eexists exists f_equal refine instantiate revert simpl specialize generalize dependent red induction beta iota zeta delta exfalso autorewrite setoid_rewrite compute vm_compute native_compute ) end
def self.tacticals
def self.tacticals @tacticals ||= Set.new %w( repeat first try ) end
def self.terminators
def self.terminators @terminators ||= Set.new %w( omega solve congruence reflexivity exact assumption eassumption ) end