"" " for theorem-proving languages.for details."" " from pygments.lexer import RegexLexer, bygroups, default, wordsfrom pygments.token import Text, Comment, Operator, Keyword, Name, String, \# compatibility import from pygments.lexers.lean import LeanLexer # noqa: F401 'CoqLexer' , 'IsabelleLexer' ]class CoqLexer(RegexLexer):"" " For the Coq theorem prover."" " 'Coq' 'http://coq.inria.fr/ ' 'coq' ]'*.v' ]'text/x-coq' ]'1.5' # no re.MULTILINE # Vernacular commands 'Section' , 'Module' , 'End' , 'Require' , 'Import' , 'Export' , 'Include' , 'Variable' ,'Variables' , 'Parameter' , 'Parameters' , 'Axiom' , 'Axioms' , 'Hypothesis' ,'Hypotheses' , 'Notation' , 'Local' , 'Tactic' , 'Reserved' , 'Scope' ,'Open' , 'Close' , 'Bind' , 'Declare' , 'Delimit' , 'Definition' , 'Example' , 'Let' ,'Ltac' , 'Ltac2' , 'Fixpoint' , 'CoFixpoint' , 'Morphism' , 'Relation' , 'Implicit' ,'Arguments' , 'Types' , 'Contextual' , 'Strict' , 'Prenex' ,'Implicits' , 'Inductive' , 'CoInductive' , 'Record' , 'Structure' ,'Variant' , 'Canonical' , 'Coercion' , 'Theorem' , 'Lemma' , 'Fact' ,'Remark' , 'Corollary' , 'Proposition' , 'Property' , 'Goal' ,'Proof' , 'Restart' , 'Save' , 'Qed' , 'Defined' , 'Abort' , 'Admitted' ,'Hint' , 'Resolve' , 'Rewrite' , 'View' , 'Search' , 'Compute' , 'Eval' ,'Show' , 'Print' , 'Printing' , 'All' , 'Graph' , 'Projections' , 'inside' ,'outside' , 'Check' , 'Global' , 'Instance' , 'Class' , 'Existing' ,'Universe' , 'Polymorphic' , 'Monomorphic' , 'Context' , 'Scheme' , 'From' ,'Undo' , 'Fail' , 'Function' , 'Program' , 'Elpi' , 'Extract' , 'Opaque' ,'Transparent' , 'Unshelve' , 'Next Obligation' ,# Gallina 'forall' , 'exists' , 'exists2' , 'fun' , 'fix' , 'cofix' , 'struct' ,'match' , 'end' , 'in' , 'return' , 'let' , 'if' , 'is' , 'then' , 'else' ,'for' , 'of' , 'nosimpl' , 'with' , 'as' ,# Sorts 'Type' , 'Prop' , 'SProp' , 'Set' ,# Tactics 'pose' , 'set' , 'move' , 'case' , 'elim' , 'apply' , 'clear' , 'hnf' , 'intro' ,'intros' , 'generalize' , 'rename' , 'pattern' , 'after' , 'destruct' ,'induction' , 'using' , 'refine' , 'inversion' , 'injection' , 'rewrite' ,'congr' , 'unlock' , 'compute' , 'ring' , 'field' , 'replace' , 'fold' ,'unfold' , 'change' , 'cutrewrite' , 'simpl' , 'have' , 'suff' , 'wlog' ,'suffices' , 'without' , 'loss' , 'nat_norm' , 'assert' , 'cut' , 'trivial' ,'revert' , 'bool_congr' , 'nat_congr' , 'symmetry' , 'transitivity' , 'auto' ,'split' , 'left' , 'right' , 'autorewrite' , 'tauto' , 'setoid_rewrite' ,'intuition' , 'eauto' , 'eapply' , 'econstructor' , 'etransitivity' ,'constructor' , 'erewrite' , 'red' , 'cbv' , 'lazy' , 'vm_compute' ,'native_compute' , 'subst' ,# Terminators 'by' , 'now' , 'done' , 'exact' , 'reflexivity' ,'tauto' , 'romega' , 'omega' , 'lia' , 'nia' , 'lra' , 'nra' , 'psatz' ,'assumption' , 'solve' , 'contradiction' , 'discriminate' ,'congruence' , 'admit' # Control 'do' , 'last' , 'first' , 'try' , 'idtac' , 'repeat' ,# 'as', 'assert', 'begin', 'class', 'constraint', 'do', 'done', # 'downto', 'else', 'end', 'exception', 'external', 'false', # 'for', 'fun', 'function', 'functor', 'if', 'in', 'include', # 'inherit', 'initializer', 'lazy', 'let', 'match', 'method', # 'module', 'mutable', 'new', 'object', 'of', 'open', 'private', # 'raise', 'rec', 'sig', 'struct', 'then', 'to', 'true', 'try', # 'type', 'val', 'virtual', 'when', 'while', 'with' '!=' , '#', '&', '&&', r'\(', r'\)', r'\*', r'\+', ',', '-', r'-\.', '->' , r'\.' , r'\.\.' , ':' , '::' , ':=' , ':>' , ';' , ';;' , '<' , '<-' ,'<->' , '=' , '>' , '>]' , r'>\}' , r'\?' , r'\?\?' , r'\[' , r'\[<' , r'\[>' ,'\[\|' , ']' , '_' , '`' , r'\{' , r'\{<' , r'lp:\{\{' , r'\|' , r'\|]' , r'\}' , '~' , '=>' ,'/\\' , r'\\/' , r'\{\|' , r'\|\}' ,# 'Π', 'Σ', # Not defined in the standard library 'λ' , '¬' , '∧' , '∨' , '∀' , '∃' , '→' , '↔' , '≠' , '≤' , '≥' ,'[!$%&*+\./:<=>?@^|~-]' '[!?~]' '[=<>@^|&+\*/$%-]' 'root' : ['\s+' , Text),'false|true|\(\)|\[\]' , Name.Builtin.Pseudo),'\(\*' , Comment, 'comment' ),'\b(?:[^\W\d][\w\' ]*\.)+[^\W\d][\w\']*\b' , Name),'\bEquations\b\??' , Keyword.Namespace),'\b(Elpi)(\s+)(Program|Query|Accumulate|Command|Typecheck|Db|Export|Tactic)?\b' , bygroups(Keyword.Namespace,Text,Keyword.Namespace)),# Very weak heuristic to distinguish the Set vernacular from the Set sort '\bUnset\b|\bSet(?=[ \t]+[A-Z][a-z][^\n]*?\.)' , Keyword.Namespace, 'set-options' ),'\b(?:String|Number)\s+Notation' , Keyword.Namespace, 'sn-notation' ),'\b' , suffix=r'\b' ), Keyword.Namespace),'\b' , suffix=r'\b' ), Keyword),'\b' , suffix=r'\b' ), Keyword.Type),'\b' , suffix=r'\b' ), Keyword),'\b' , suffix=r'\b' ), Keyword.Pseudo),'\b' , suffix=r'\b' ), Keyword.Reserved),# (r'\b([A-Z][\w\']*)(\.)', Name.Namespace, 'dotted'), '\b([A-Z][\w\' ]*)', Name), '({})' .format('|' .join(keyopts[::-1])), Operator),'({infix_syms}|{prefix_syms})?{operators}' , Operator),"[^\W\d][\w']*" , Name),'\d[\d_]*' , Number.Integer),'0[xX][\da-fA-F][\da-fA-F_]*' , Number.Hex),'0[oO][0-7][0-7_]*' , Number.Oct),'0[bB][01][01_]*' , Number.Bin),'-?\d[\d_]*(.[\d_]*)?([eE][+\-]?\d[\d_]*)' , Number.Float),"'(?:(\\[\\\" 'ntbr ])|(\\[0-9]{3})|(\\x[0-9a-fA-F]{2}))' ", String.Char), "'.'" , String.Char),"'" , Keyword), # a stray quote is another syntax element '"' , String.Double, 'string' ),'[~?][a-z][\w\' ]*:', Name), '\S' , Name.Builtin.Pseudo),'set-options' : ['\s+' , Text),'[A-Z]\w*' , Keyword.Namespace),'"' , String.Double, 'string' ),'\d+' , Number.Integer),'\.' , Punctuation, '#pop'), 'sn-notation' : ['\s+' , Text),# Extra keywords to highlight only in this scope '\b(?:via|mapping|abstract|warning|after)\b' , Keyword),'=>|[()\[\]:,]' , Operator),'\b[^\W\d][\w\' ]*(?:\.[^\W\d][\w\']*)*\b' , Name),'\d[\d_]*' , Number.Integer),'0[xX][\da-fA-F][\da-fA-F_]*' , Number.Hex),'\(\*' , Comment, 'comment' ),'\.' , Punctuation, '#pop'), 'comment' : [# Consume comments like ***** as one token '([^(*)]+|\*+(?!\)))+' , Comment),'\(\*' , Comment, '#push'), '\*\)' , Comment, '#pop'), '[(*)]' , Comment),'string' : ['[^"]+' , String.Double),'""' , String.Double),'"' , String.Double, '#pop'), 'dotted' : ['\s+' , Text),'\.' , Punctuation),'[A-Z][\w\' ]*(?=\s*\.)', Name.Namespace), '[A-Z][\w\' ]*', Name.Class, ' #pop'), '[a-z][a-z0-9_\' ]*', Name, ' #pop'), '#pop') def analyse_text(text):if 'Qed' in text and 'Proof' in text:return 1class IsabelleLexer(RegexLexer):"" " For the Isabelle proof assistant."" " 'Isabelle' 'https://isabelle.in.tum.de/ ' 'isabelle' ]'*.thy' ]'text/x-isabelle' ]'2.0' 'and' , 'assumes' , 'attach' , 'avoids' , 'binder' , 'checking' ,'class_instance' , 'class_relation' , 'code_module' , 'congs' ,'constant' , 'constrains' , 'datatypes' , 'defines' , 'file' , 'fixes' ,'for' , 'functions' , 'hints' , 'identifier' , 'if' , 'imports' , 'in' ,'includes' , 'infix' , 'infixl' , 'infixr' , 'is' , 'keywords' , 'lazy' ,'module_name' , 'monos' , 'morphisms' , 'no_discs_sels' , 'notes' ,'obtains' , 'open' , 'output' , 'overloaded' , 'parametric' , 'permissive' ,'pervasive' , 'rep_compat' , 'shows' , 'structure' , 'type_class' ,'type_constructor' , 'unchecked' , 'unsafe' , 'where' ,'ML_command' , 'ML_val' , 'class_deps' , 'code_deps' , 'code_thms' ,'display_drafts' , 'find_consts' , 'find_theorems' , 'find_unused_assms' ,'full_prf' , 'help' , 'locale_deps' , 'nitpick' , 'pr' , 'prf' ,'print_abbrevs' , 'print_antiquotations' , 'print_attributes' ,'print_binds' , 'print_bnfs' , 'print_bundles' ,'print_case_translations' , 'print_cases' , 'print_claset' ,'print_classes' , 'print_codeproc' , 'print_codesetup' ,'print_coercions' , 'print_commands' , 'print_context' ,'print_defn_rules' , 'print_dependencies' , 'print_facts' ,'print_induct_rules' , 'print_inductives' , 'print_interps' ,'print_locale' , 'print_locales' , 'print_methods' , 'print_options' ,'print_orders' , 'print_quot_maps' , 'print_quotconsts' ,'print_quotients' , 'print_quotientsQ3' , 'print_quotmapsQ3' ,'print_rules' , 'print_simpset' , 'print_state' , 'print_statement' ,'print_syntax' , 'print_theorems' , 'print_theory' , 'print_trans_rules' ,'prop' , 'pwd' , 'quickcheck' , 'refute' , 'sledgehammer' , 'smt_status' ,'solve_direct' , 'spark_status' , 'term' , 'thm' , 'thm_deps' , 'thy_deps' ,'try' , 'try0' , 'typ' , 'unused_thms' , 'value' , 'values' , 'welcome' ,'print_ML_antiquotations' , 'print_term_bindings' , 'values_prolog' ,'theory' , 'begin' , 'end' )'header' , 'chapter' )'section' , 'subsection' , 'subsubsection' , 'sect' , 'subsect' ,'subsubsect' ,'ML' , 'ML_file' , 'abbreviation' , 'adhoc_overloading' , 'arities' ,'atom_decl' , 'attribute_setup' , 'axiomatization' , 'bundle' ,'case_of_simps' , 'class' , 'classes' , 'classrel' , 'codatatype' ,'code_abort' , 'code_class' , 'code_const' , 'code_datatype' ,'code_identifier' , 'code_include' , 'code_instance' , 'code_modulename' ,'code_monad' , 'code_printing' , 'code_reflect' , 'code_reserved' ,'code_type' , 'coinductive' , 'coinductive_set' , 'consts' , 'context' ,'datatype' , 'datatype_new' , 'datatype_new_compat' , 'declaration' ,'declare' , 'default_sort' , 'defer_recdef' , 'definition' , 'defs' ,'domain' , 'domain_isomorphism' , 'domaindef' , 'equivariance' ,'export_code' , 'extract' , 'extract_type' , 'fixrec' , 'fun' ,'fun_cases' , 'hide_class' , 'hide_const' , 'hide_fact' , 'hide_type' ,'import_const_map' , 'import_file' , 'import_tptp' , 'import_type_map' ,'inductive' , 'inductive_set' , 'instantiation' , 'judgment' , 'lemmas' ,'lifting_forget' , 'lifting_update' , 'local_setup' , 'locale' ,'method_setup' , 'nitpick_params' , 'no_adhoc_overloading' ,'no_notation' , 'no_syntax' , 'no_translations' , 'no_type_notation' ,'nominal_datatype' , 'nonterminal' , 'notation' , 'notepad' , 'oracle' ,'overloading' , 'parse_ast_translation' , 'parse_translation' ,'partial_function' , 'primcorec' , 'primrec' , 'primrec_new' ,'print_ast_translation' , 'print_translation' , 'quickcheck_generator' ,'quickcheck_params' , 'realizability' , 'realizers' , 'recdef' , 'record' ,'refute_params' , 'setup' , 'setup_lifting' , 'simproc_setup' ,'simps_of_case' , 'sledgehammer_params' , 'spark_end' , 'spark_open' ,'spark_open_siv' , 'spark_open_vcg' , 'spark_proof_functions' ,'spark_types' , 'statespace' , 'syntax' , 'syntax_declaration' , 'text' ,'text_raw' , 'theorems' , 'translations' , 'type_notation' ,'type_synonym' , 'typed_print_translation' , 'typedecl' , 'hoarestate' ,'install_C_file' , 'install_C_types' , 'wpc_setup' , 'c_defs' , 'c_types' ,'memsafe' , 'SML_export' , 'SML_file' , 'SML_import' , 'approximate' ,'bnf_axiomatization' , 'cartouche' , 'datatype_compat' ,'free_constructors' , 'functor' , 'nominal_function' ,'nominal_termination' , 'permanent_interpretation' ,'binds' , 'defining' , 'smt2_status' , 'term_cartouche' ,'boogie_file' , 'text_cartouche' ,'inductive_cases' , 'inductive_simps' )'ax_specification' , 'bnf' , 'code_pred' , 'corollary' , 'cpodef' ,'crunch' , 'crunch_ignore' ,'enriched_type' , 'function' , 'instance' , 'interpretation' , 'lemma' ,'lift_definition' , 'nominal_inductive' , 'nominal_inductive2' ,'nominal_primrec' , 'pcpodef' , 'primcorecursive' ,'quotient_definition' , 'quotient_type' , 'recdef_tc' , 'rep_datatype' ,'schematic_corollary' , 'schematic_lemma' , 'schematic_theorem' ,'spark_vc' , 'specification' , 'subclass' , 'sublocale' , 'termination' ,'theorem' , 'typedef' , 'wrap_free_constructors' ,'by' , 'done' , 'qed' )'sorry' , 'oops' )'have' , 'hence' , 'interpret' )'next' , 'proof' )'finally' , 'from' , 'then' , 'ultimately' , 'with' ,'ML_prf' , 'also' , 'include' , 'including' , 'let' , 'moreover' , 'note' ,'txt' , 'txt_raw' , 'unfolding' , 'using' , 'write' ,'assume' , 'case' , 'def' , 'fix' , 'presume' )'guess' , 'obtain' , 'show' , 'thus' )'apply' , 'apply_end' , 'apply_trace' , 'back' , 'defer' , 'prefer' ,'::' , ':' , '(' , ')' , '[' , ']' , '_' , '=' , ',' , '|' ,'+' , '-' , '!' , '?' ,'{' , '}' , '.' , '..' )'root' : ['\s+' , Whitespace),'\(\*' , Comment, 'comment' ),'\\' , String.Symbol, 'cartouche' ),'\{\*|‹' , String, 'cartouche' ),'\b' , suffix=r'\b' ), Keyword.Pseudo),'\b' , suffix=r'\b' ), Keyword.Type),'\b' , suffix=r'\b' ), Keyword),'\b' , suffix=r'\b' ), Keyword),'\b' , suffix=r'\b' ), Generic.Heading),'\b' , suffix=r'\b' ), Generic.Subheading),'\b' , suffix=r'\b' ), Keyword.Namespace),'\b' , suffix=r'\b' ), Keyword.Namespace),'\b' , suffix=r'\b' ), Generic.Error),'\b' , suffix=r'\b' ), Keyword),'\b' , suffix=r'\b' ), Keyword),'\b' , suffix=r'\b' ), Keyword),'\b' , suffix=r'\b' ), Keyword),'\b' , suffix=r'\b' ), Keyword),'\b' , suffix=r'\b' ), Keyword),'\b' , suffix=r'\b' ), Keyword),'\b' , suffix=r'\b' ), Keyword.Pseudo),'\\<(\w|\^)*>' , Text.Symbol),"'[^\W\d][.\w']*" , Name.Type),'0[xX][\da-fA-F][\da-fA-F_]*' , Number.Hex),'0[oO][0-7][0-7_]*' , Number.Oct),'0[bB][01][01_]*' , Number.Bin),'"' , String, 'string' ),'`' , String.Other, 'fact' ),'[^\s:|\[\]\-()=,+!?{}._][^\s:|\[\]\-()=,+!?{}]*' , Name),'comment' : ['[^(*)]+' , Comment),'\(\*' , Comment, '#push'), '\*\)' , Comment, '#pop'), '[(*)]' , Comment),'cartouche' : ['[^{*}\\‹›]+' , String),'\\' , String.Symbol, '#push'), '\{\*|‹' , String, '#push'), '\\' , String.Symbol, '#pop'), '\*\}|›' , String, '#pop'), '\\<(\w|\^)*>' , String.Symbol),'[{*}\\]' , String),'string' : ['[^"\\]+' , String),'\\<(\w|\^)*>' , String.Symbol),'\\"' , String),'\\' , String),'"' , String, '#pop'), 'fact' : ['[^`\\]+' , String.Other),'\\<(\w|\^)*>' , String.Symbol),'\\`' , String.Other),'\\' , String.Other),'`' , String.Other, '#pop'), quality 70%
¤ Dauer der Verarbeitung: 0.50 Sekunden
¤ *© Formatika GbR, Deutschland
