| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/Roqc/plugins/ltac2/ (Beweissystem des Inria Version 9.1.0©) Datei vom 15.8.2025 mit Größe 4 kB |
|
Quelle tac2qexpr.mli Sprache: SML |
|||||||||
|
(************************************************************************)
(* * The Rocq Prover / The Rocq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) (* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names open Tac2expr (** Quoted variants of Ltac syntactic categories. Contrarily to the former, they sometimes allow anti-quotations. Used for notation syntax classes. *) type 'a or_anti = | QExpr of 'a | QAnti of Id.t CAst.t type reference_r = | QReference of Libnames.qualid | QHypothesis of Id.t type reference = reference_r CAst.t type quantified_hypothesis = | QAnonHyp of int CAst.t | QNamedHyp of Id.t CAst.t type bindings_r = | QImplicitBindings of Constrexpr.constr_expr list | QExplicitBindings of (quantified_hypothesis CAst.t or_anti * Constrexpr.constr_expr) C | QNoBindings type bindings = bindings_r CAst.t type intro_pattern_r = | QIntroForthcoming of bool | QIntroNaming of intro_pattern_naming | QIntroAction of intro_pattern_action and intro_pattern_naming_r = | QIntroIdentifier of Id.t CAst.t or_anti | QIntroFresh of Id.t CAst.t or_anti | QIntroAnonymous and intro_pattern_action_r = | QIntroWildcard | QIntroOrAndPattern of or_and_intro_pattern | QIntroInjection of intro_pattern list CAst.t | QIntroApplyOn of Constrexpr.constr_expr * intro_pattern | QIntroRewrite of bool and or_and_intro_pattern_r = | QIntroOrPattern of intro_pattern list CAst.t list | QIntroAndPattern of intro_pattern list CAst.t and intro_pattern = intro_pattern_r CAst.t and intro_pattern_naming = intro_pattern_naming_r CAst.t and intro_pattern_action = intro_pattern_action_r CAst.t and or_and_intro_pattern = or_and_intro_pattern_r CAst.t type occurrences_r = | QAllOccurrences | QAllOccurrencesBut of int CAst.t or_anti list | QNoOccurrences | QOnlyOccurrences of int CAst.t or_anti list type occurrences = occurrences_r CAst.t type hyp_location = (occurrences * Id.t CAst.t or_anti) * Locus.hyp_location_flag type clause_r = { q_onhyps : hyp_location list option; q_concl_occs : occurrences; } type clause = clause_r CAst.t type constr_with_bindings = (Constrexpr.constr_expr * bindings) CAst.t type destruction_arg_r = | QElimOnConstr of constr_with_bindings | QElimOnIdent of Id.t CAst.t | QElimOnAnonHyp of int CAst.t type destruction_arg = destruction_arg_r CAst.t type induction_clause_r = { indcl_arg : destruction_arg; indcl_eqn : intro_pattern_naming option; indcl_as : or_and_intro_pattern option; indcl_in : clause option; } type induction_clause = induction_clause_r CAst.t type conversion_r = | QConvert of Constrexpr.constr_expr | QConvertWith of Constrexpr.constr_expr * Constrexpr.constr_expr type conversion = conversion_r CAst.t type multi_r = | QPrecisely of int CAst.t | QUpTo of int CAst.t | QRepeatStar | QRepeatPlus type multi = multi_r CAst.t type orientation = bool option CAst.t type rewriting_r = { rew_orient : orientation; rew_repeat : multi; rew_equatn : constr_with_bindings; } type rewriting = rewriting_r CAst.t type dispatch_r = raw_tacexpr option list * (raw_tacexpr option * raw_tacexpr option list) op type dispatch = dispatch_r CAst.t type red_flag_r = | QBeta | QIota | QMatch | QFix | QCofix | QZeta | QConst of reference or_anti list CAst.t | QDeltaBut of reference or_anti list CAst.t | QHead type red_flag = red_flag_r CAst.t type strategy_flag = red_flag list CAst.t type constr_match_pattern_r = | QConstrMatchPattern of Constrexpr.constr_expr | QConstrMatchContext of Id.t option * Constrexpr.constr_expr type constr_match_pattern = constr_match_pattern_r CAst.t type constr_match_branch = (constr_match_pattern * raw_tacexpr) CAst.t type constr_matching = constr_match_branch list CAst.t type goal_match_pattern_r = { q_goal_match_concl : constr_match_pattern; q_goal_match_hyps : (Names.lname * constr_match_pattern option * constr_match_pattern) l } type goal_match_pattern = goal_match_pattern_r CAst.t type goal_match_branch = (goal_match_pattern * raw_tacexpr) CAst.t type goal_matching = goal_match_branch list CAst.t type hintdb_r = | QHintAll | QHintDbs of Id.t CAst.t or_anti list type hintdb = hintdb_r CAst.t type move_location_r = | QMoveAfter of Id.t CAst.t or_anti | QMoveBefore of Id.t CAst.t or_anti | QMoveFirst | QMoveLast type move_location = move_location_r CAst.t type pose = (Id.t CAst.t or_anti option * Constrexpr.constr_expr) CAst.t type assertion_r = | QAssertType of intro_pattern option * Constrexpr.constr_expr * raw_tacexpr option | QAssertValue of Id.t CAst.t or_anti * Constrexpr.constr_expr type assertion = assertion_r CAst.t ¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28