Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


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) CAst.t list
| 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) option

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) list;
}

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

quality100%

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.