(************************************************************************) (* * 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) *) (************************************************************************)
(** 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} *)
(** 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 withtype'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.20 Sekunden
(vorverarbeitet)
¤
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.
