| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/pretyping/ (Beweissystem des Inria Version 9.1.0©) Datei vom 15.8.2025 mit Größe 1 kB |
|
Quelle templateArity.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 EConstr type template_binder = { bind_sort : Sorts.t; default : Sorts.t; } (** NB: the types and rel_contexts may mention previous args eg "sigT : forall A, (A -> Type) -> Type" is "TemplateArg ([], u, TemplateArg ([_:Rel 1], v, IndType (_, [], Type@{max(u,v)})))" note the "Rel 1" *) type template_arity = | NonTemplateArg of Name.t binder_annot * types * template_arity | TemplateArg of Name.t binder_annot * rel_context * template_binder * template_arity | DefParam of Name.t binder_annot * constr * types * template_arity | CtorType of Declarations.template_universes * types | IndType of Declarations.template_universes * rel_context * Sorts.t val get_template_arity : Environ.env -> Names.inductive -> ctoropt:int option -> template_arity ¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28