class Rouge::Lexers::Coq
Public Class Methods
classify(x)
click to toggle source
# File lib/rouge/lexers/coq.rb, line 57 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
coq()
click to toggle source
# File lib/rouge/lexers/coq.rb, line 17 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 Admitted ) end
gallina()
click to toggle source
# File lib/rouge/lexers/coq.rb, line 10 def self.gallina @gallina ||= Set.new %w( as fun if in let match then else return end Type Set Prop forall ) end
ltac()
click to toggle source
# File lib/rouge/lexers/coq.rb, line 30 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
tacticals()
click to toggle source
# File lib/rouge/lexers/coq.rb, line 44 def self.tacticals @tacticals ||= Set.new %w( repeat first try ) end
terminators()
click to toggle source
# File lib/rouge/lexers/coq.rb, line 50 def self.terminators @terminators ||= Set.new %w( omega solve congruence reflexivity exact assumption eassumption ) end