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

(** This family of functions assumes its constr argument is known to be
   well-typable. It does not type-check, just recompute the type
   without any costly verifications. On non well-typable terms, it
   either produces a wrong result or raise an anomaly. Use with care.
   It doesn't handle predicative universes too. *)

(** The "polyprop" optional argument is used by the extraction to
    disable "Prop-polymorphism" *)

(** The "lax" optional argument provides a relaxed version of
    [get_type_of] that won't raise any anomaly but RetypeError instead *)

type retype_error
exception RetypeError of retype_error

val get_type_of :
  ?metas:(Constr.metavariable -> types option) ->
  ?polyprop:bool -> ?lax:bool -> env -> evar_map -> constr -> types

(** No-evar version of [get_type_of] *)
val get_type_of_constr : ?polyprop:bool -> ?lax:bool
  -> env -> ?uctx:UState.t -> Constr.t -> Constr.types

val get_sort_of :
  ?polyprop:bool -> env -> evar_map -> types -> ESorts.t

val get_sort_quality_of :
  ?polyprop:bool -> env -> evar_map -> types -> UnivGen.QualityOrSet.t

(** Makes an unsafe judgment from a constr *)
val get_judgment_of : env -> evar_map -> constr -> unsafe_judgment

val type_of_global_reference_knowing_parameters : env -> evar_map -> constr ->
  constr array -> types

val sorts_of_context : env -> evar_map -> rel_context -> ESorts.t list

val expand_projection : env -> evar_map -> Names.Projection.t -> constr -> constr list -> constr

val reinterpret_get_type_of : src:Names.Id.t -> env -> evar_map -> constr -> types

val print_retype_error : retype_error -> Pp.t

val relevance_of_projection_repr : env -> Names.Projection.Repr.t EConstr.puniverses -> ERelevance.t

val relevance_of_term : env -> evar_map -> constr -> ERelevance.t
val relevance_of_type : env -> evar_map -> types -> ERelevance.t
val relevance_of_sort : ESorts.t -> ERelevance.t

val is_term_irrelevant : env -> Evd.evar_map -> Evd.econstr -> bool

(** The "polyprop" optional argument above controls
    the "Prop-polymorphism". By default, it is allowed.
    But when "polyprop=false", the following exception is raised
    when a polymorphic singleton inductive type becomes Prop due to
    parameter instantiation. This is used by the Ocaml extraction,
    which cannot handle (yet?) Prop-polymorphism. *)

exception SingletonInductiveBecomesProp of Names.inductive

quality100%

¤ Dauer der Verarbeitung: 0.4 Sekunden ¤

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.