Quelle combinators.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 Environ
open Evd
open EConstr

(** [telescope env sigma ctx] turns a context [x1:A1;...;xn:An] into a
    right-associated nested sigma-type of the right sort. It returns:
    - the nested sigma-type [T := {x1:A1 & ... {xn-1:An-1 & ... An} ... }]
    - the canonical tuple [(existsT _ x1 ... (existsT _ xn-1 xn) ...)]
      inhabiting the sigma-type in the given context
    - an instantiation of the assumptions of [ctx] with values they
      have in the context [x:T], that is
      [x1:=projT1 x;...;xn-1:=projT1 ... (projT2 x);xn:=projT2 ... (projT2 x)];
      note that let-ins in the original context are preserved
    Depending on the sorts of types, it uses either [ex], [sig] or
    [sigT], even if we always used [sigT] above as an example.
*)

type telescope = {
  telescope_type : types;
  telescope_value : constr;
}

val telescope : env -> evar_map -> rel_context -> evar_map * rel_context * telescope

(** [make_iterated_tuple env sigma ~default c] encapsulates [c] (of
    inferred type [C]) and its free variables [x1,...,xn] into a
    right-associated nested tuple in a [sigT]-type. It returns:
    - the nested type [{x1:A1 & ... {xn:An & ... C} ... }]
    - the tuple [(existsT _ x1 ... (existsT _ xn c) ...)]
    - an alternative tuple [(existsT _ x1 ... (existsT _ xn default) ...)];
      if [default] has not the right type, it fails.
*)

val make_iterated_tuple : env -> evar_map -> default:constr -> constr -> types -> evar_map * telescope * constr

(** [make_selector env sigma ~pos ~special ~default c] constructs a
    case-split on [c] (assumed of inductive type), with the [pos]-th
    branch returning [special], and all the other branch returning
    [default]. *)

val make_selector : env -> evar_map -> pos:int -> special:constr -> default:constr -> constr -> types -> constr

quality97%

¤ Dauer der Verarbeitung: 0.1 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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.