# File lib/rouge/lexers/coq.rb, line 10 def self.analyze_text(text) return 0.3 if text.include? "Require" end
# File lib/rouge/lexers/coq.rb, line 71 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
# File lib/rouge/lexers/coq.rb, line 21 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
# File lib/rouge/lexers/coq.rb, line 67 def self.end_sentence @end_sentence ||= Punctuation::Indicator end
# File lib/rouge/lexers/coq.rb, line 14 def self.gallina @gallina ||= Set.new %w( as fun if in let match then else return end Type Set Prop forall ) end
# File lib/rouge/lexers/coq.rb, line 61 def self.keyopts @keyopts ||= Set.new %w( := => -> /\\ \\/ _ ; :> : ) end
# File lib/rouge/lexers/coq.rb, line 34 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
# File lib/rouge/lexers/coq.rb, line 48 def self.tacticals @tacticals ||= Set.new %w( repeat first try ) end
# File lib/rouge/lexers/coq.rb, line 54 def self.terminators @terminators ||= Set.new %w( omega solve congruence reflexivity exact assumption eassumption ) end