Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: ftactic.mli Sprache: SML

Original von: Coq^©

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \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)         *)
(************************************************************************)

(** This module defines potentially focussing tactics. They are used by Ltac to
    emulate the historical behaviour of always-focussed tactics while still
    allowing to remain global when the goal is not needed. *)

type +'a focus

type +'a t = 'a focus Proofview.tactic
(** The type of focussing tactics. A focussing tactic is like a normal tactic,
    except that it is able to remember it have entered a goal. Whenever this is
    the case, each subsequent effect of the tactic is dispatched on the
    focused goals. This is a monad. *)

(** {5 Monadic interface} *)

val return : 'a -> 'a t
(** The unit of the monad. *)

val bind : 'a t -> ('a -> 'b t) -> 'b t
(** The bind of the monad. *)

(** {5 Operations} *)

val lift : 'a Proofview.tactic -> 'a t
(** Transform a tactic into a focussing tactic. The resulting tactic is not
    focused. *)

val run : 'a t -> ('a -> unit Proofview.tactic) -> unit Proofview.tactic
(** Given a continuation producing a tactic, evaluates the focussing tactic. If
    the tactic has not focused, then the continuation is evaluated once.
    Otherwise it is called in each of the currently focused goals. *)

(** {5 Focussing} *)

val nf_enter : (Proofview.Goal.t -> 'a t) -> 'a t
[@@ocaml.deprecated "Normalization is enforced by EConstr, please use [enter]"]

(** Enter a goal. The resulting tactic is focused. *)

val enter : (Proofview.Goal.t -> 'a t) -> 'a t
(** Enter a goal, without evar normalization. The resulting tactic is
    focused. *)

val with_env : 'a t -> (Environ.env*'a) t
(** [with_env t] returns, in addition to the return type of [t], an
    environment, which is the global environment if [t] does not focus on
    goals, or the local goal environment if [t] focuses on goals. *)

(** {5 Notations} *)

val (>>=) : 'a t -> ('a -> 'b t) -> 'b t
(** Notation for {!bind}. *)

val (<*>) : unit t -> 'a t -> 'a t
(** Sequence. *)

(** {5 List operations} *)

module List : Monad.ListS with type 'a t := 'a t

(** {5 Notations} *)

module Notations :
sig
  val (>>=) : 'a t -> ('a -> 'b t) -> 'b t
  val (<*>) : unit t -> 'a t -> 'a t
end

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.