class Rouge::Lexers::Coq
Public Class Methods
classify(x)
click to toggle source
# File lib/rouge/lexers/coq.rb, line 68 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 18 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
end_sentence()
click to toggle source
# File lib/rouge/lexers/coq.rb, line 64 def self.end_sentence @end_sentence ||= Punctuation::Indicator end
gallina()
click to toggle source
# File lib/rouge/lexers/coq.rb, line 11 def self.gallina @gallina ||= Set.new %w( as fun if in let match then else return end Type Set Prop forall ) end
keyopts()
click to toggle source
# File lib/rouge/lexers/coq.rb, line 58 def self.keyopts @keyopts ||= Set.new %w( := => -> /\\ \\/ _ ; :> : ) end
ltac()
click to toggle source
# File lib/rouge/lexers/coq.rb, line 31 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 45 def self.tacticals @tacticals ||= Set.new %w( repeat first try ) end
terminators()
click to toggle source
# File lib/rouge/lexers/coq.rb, line 51 def self.terminators @terminators ||= Set.new %w( omega solve congruence reflexivity exact assumption eassumption ) end