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

(** Operations for handling terms under a local typing context. *)

open Evd

(** Variants of [Tacmach] functions built with the new proof engine *)

val pf_apply : (env -> evar_map -> 'a) -> Proofview.Goal.t -> 'a

val project : Proofview.Goal.t -> Evd.evar_map
val pf_env : Proofview.Goal.t -> Environ.env
val pf_concl : Proofview.Goal.t -> types

(** This function does no type inference and expects an already well-typed term.
    It recomputes its type in the fastest way possible (no conversion is ever involved) *)
val pf_get_type_of : Proofview.Goal.t -> constr -> types

(** This function entirely type-checks the term and computes its type
    and the implied universe constraints. *)
val pf_type_of : Proofview.Goal.t -> constr -> evar_map * types
val pf_conv_x : Proofview.Goal.t -> t -> t -> bool

val pf_get_new_id  : Id.t -> Proofview.Goal.t -> Id.t
val pf_ids_of_hyps : Proofview.Goal.t -> Id.t list
val pf_ids_set_of_hyps : Proofview.Goal.t -> Id.Set.t
val pf_hyps_types : Proofview.Goal.t -> (Id.t * types) list

val pf_get_hyp : Id.t -> Proofview.Goal.t -> named_declaration
val pf_get_hyp_typ        : Id.t -> Proofview.Goal.t -> types
val pf_last_hyp           : Proofview.Goal.t -> named_declaration

val pf_nf_concl : Proofview.Goal.t -> types

val pf_hnf_constr : Proofview.Goal.t -> constr -> types
val pf_hnf_type_of : Proofview.Goal.t -> constr -> types

val pf_compute : Proofview.Goal.t -> constr -> constr
val pf_whd_compute : Proofview.Goal.t -> constr -> constr

val pf_nf_evar : Proofview.Goal.t -> constr -> constr

val pr_gls : Proofview.Goal.t -> Pp.t

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.