basant307/AI_Governance_Project

1/*2Language: Coq3Author: Stephan Boyer <stephan@stephanboyer.com>4Category: functional5Website: https://coq.inria.fr6*/7 8/** @type LanguageFn */9function coq(hljs) {10  const KEYWORDS = [11    "_|0",12    "as",13    "at",14    "cofix",15    "else",16    "end",17    "exists",18    "exists2",19    "fix",20    "for",21    "forall",22    "fun",23    "if",24    "IF",25    "in",26    "let",27    "match",28    "mod",29    "Prop",30    "return",31    "Set",32    "then",33    "Type",34    "using",35    "where",36    "with",37    "Abort",38    "About",39    "Add",40    "Admit",41    "Admitted",42    "All",43    "Arguments",44    "Assumptions",45    "Axiom",46    "Back",47    "BackTo",48    "Backtrack",49    "Bind",50    "Blacklist",51    "Canonical",52    "Cd",53    "Check",54    "Class",55    "Classes",56    "Close",57    "Coercion",58    "Coercions",59    "CoFixpoint",60    "CoInductive",61    "Collection",62    "Combined",63    "Compute",64    "Conjecture",65    "Conjectures",66    "Constant",67    "constr",68    "Constraint",69    "Constructors",70    "Context",71    "Corollary",72    "CreateHintDb",73    "Cut",74    "Declare",75    "Defined",76    "Definition",77    "Delimit",78    "Dependencies",79    "Dependent",80    "Derive",81    "Drop",82    "eauto",83    "End",84    "Equality",85    "Eval",86    "Example",87    "Existential",88    "Existentials",89    "Existing",90    "Export",91    "exporting",92    "Extern",93    "Extract",94    "Extraction",95    "Fact",96    "Field",97    "Fields",98    "File",99    "Fixpoint",100    "Focus",101    "for",102    "From",103    "Function",104    "Functional",105    "Generalizable",106    "Global",107    "Goal",108    "Grab",109    "Grammar",110    "Graph",111    "Guarded",112    "Heap",113    "Hint",114    "HintDb",115    "Hints",116    "Hypotheses",117    "Hypothesis",118    "ident",119    "Identity",120    "If",121    "Immediate",122    "Implicit",123    "Import",124    "Include",125    "Inductive",126    "Infix",127    "Info",128    "Initial",129    "Inline",130    "Inspect",131    "Instance",132    "Instances",133    "Intro",134    "Intros",135    "Inversion",136    "Inversion_clear",137    "Language",138    "Left",139    "Lemma",140    "Let",141    "Libraries",142    "Library",143    "Load",144    "LoadPath",145    "Local",146    "Locate",147    "Ltac",148    "ML",149    "Mode",150    "Module",151    "Modules",152    "Monomorphic",153    "Morphism",154    "Next",155    "NoInline",156    "Notation",157    "Obligation",158    "Obligations",159    "Opaque",160    "Open",161    "Optimize",162    "Options",163    "Parameter",164    "Parameters",165    "Parametric",166    "Path",167    "Paths",168    "pattern",169    "Polymorphic",170    "Preterm",171    "Print",172    "Printing",173    "Program",174    "Projections",175    "Proof",176    "Proposition",177    "Pwd",178    "Qed",179    "Quit",180    "Rec",181    "Record",182    "Recursive",183    "Redirect",184    "Relation",185    "Remark",186    "Remove",187    "Require",188    "Reserved",189    "Reset",190    "Resolve",191    "Restart",192    "Rewrite",193    "Right",194    "Ring",195    "Rings",196    "Save",197    "Scheme",198    "Scope",199    "Scopes",200    "Script",201    "Search",202    "SearchAbout",203    "SearchHead",204    "SearchPattern",205    "SearchRewrite",206    "Section",207    "Separate",208    "Set",209    "Setoid",210    "Show",211    "Solve",212    "Sorted",213    "Step",214    "Strategies",215    "Strategy",216    "Structure",217    "SubClass",218    "Table",219    "Tables",220    "Tactic",221    "Term",222    "Test",223    "Theorem",224    "Time",225    "Timeout",226    "Transparent",227    "Type",228    "Typeclasses",229    "Types",230    "Undelimit",231    "Undo",232    "Unfocus",233    "Unfocused",234    "Unfold",235    "Universe",236    "Universes",237    "Unset",238    "Unshelve",239    "using",240    "Variable",241    "Variables",242    "Variant",243    "Verbose",244    "Visibility",245    "where",246    "with"247  ];248  const BUILT_INS = [249    "abstract",250    "absurd",251    "admit",252    "after",253    "apply",254    "as",255    "assert",256    "assumption",257    "at",258    "auto",259    "autorewrite",260    "autounfold",261    "before",262    "bottom",263    "btauto",264    "by",265    "case",266    "case_eq",267    "cbn",268    "cbv",269    "change",270    "classical_left",271    "classical_right",272    "clear",273    "clearbody",274    "cofix",275    "compare",276    "compute",277    "congruence",278    "constr_eq",279    "constructor",280    "contradict",281    "contradiction",282    "cut",283    "cutrewrite",284    "cycle",285    "decide",286    "decompose",287    "dependent",288    "destruct",289    "destruction",290    "dintuition",291    "discriminate",292    "discrR",293    "do",294    "double",295    "dtauto",296    "eapply",297    "eassumption",298    "eauto",299    "ecase",300    "econstructor",301    "edestruct",302    "ediscriminate",303    "eelim",304    "eexact",305    "eexists",306    "einduction",307    "einjection",308    "eleft",309    "elim",310    "elimtype",311    "enough",312    "equality",313    "erewrite",314    "eright",315    "esimplify_eq",316    "esplit",317    "evar",318    "exact",319    "exactly_once",320    "exfalso",321    "exists",322    "f_equal",323    "fail",324    "field",325    "field_simplify",326    "field_simplify_eq",327    "first",328    "firstorder",329    "fix",330    "fold",331    "fourier",332    "functional",333    "generalize",334    "generalizing",335    "gfail",336    "give_up",337    "has_evar",338    "hnf",339    "idtac",340    "in",341    "induction",342    "injection",343    "instantiate",344    "intro",345    "intro_pattern",346    "intros",347    "intuition",348    "inversion",349    "inversion_clear",350    "is_evar",351    "is_var",352    "lapply",353    "lazy",354    "left",355    "lia",356    "lra",357    "move",358    "native_compute",359    "nia",360    "nsatz",361    "omega",362    "once",363    "pattern",364    "pose",365    "progress",366    "proof",367    "psatz",368    "quote",369    "record",370    "red",371    "refine",372    "reflexivity",373    "remember",374    "rename",375    "repeat",376    "replace",377    "revert",378    "revgoals",379    "rewrite",380    "rewrite_strat",381    "right",382    "ring",383    "ring_simplify",384    "rtauto",385    "set",386    "setoid_reflexivity",387    "setoid_replace",388    "setoid_rewrite",389    "setoid_symmetry",390    "setoid_transitivity",391    "shelve",392    "shelve_unifiable",393    "simpl",394    "simple",395    "simplify_eq",396    "solve",397    "specialize",398    "split",399    "split_Rabs",400    "split_Rmult",401    "stepl",402    "stepr",403    "subst",404    "sum",405    "swap",406    "symmetry",407    "tactic",408    "tauto",409    "time",410    "timeout",411    "top",412    "transitivity",413    "trivial",414    "try",415    "tryif",416    "unfold",417    "unify",418    "until",419    "using",420    "vm_compute",421    "with"422  ];423  return {424    name: 'Coq',425    keywords: {426      keyword: KEYWORDS,427      built_in: BUILT_INS428    },429    contains: [430      hljs.QUOTE_STRING_MODE,431      hljs.COMMENT('\\(\\*', '\\*\\)'),432      hljs.C_NUMBER_MODE,433      {434        className: 'type',435        excludeBegin: true,436        begin: '\\|\\s*',437        end: '\\w+'438      },439      { // relevance booster440        begin: /[-=]>/ }441    ]442  };443}444 445export { coq as default };446