package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824

doc/rocq-runtime.engine/Ftactic/index.html

Module FtacticSource

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.

Sourcetype +'a focus

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.

Monadic interface
Sourceval return : 'a -> 'a t

The unit of the monad.

Sourceval bind : 'a t -> ('a -> 'b t) -> 'b t

The bind of the monad.

Operations
Sourceval lift : 'a Proofview.tactic -> 'a t

Transform a tactic into a focussing tactic. The resulting tactic is not focused.

Sourceval 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.

Focussing

Enter a goal. The resulting tactic is focused.

Sourceval enter : (Proofview.Goal.t -> 'a t) -> 'a t

Enter a goal, without evar normalization. The resulting tactic is focused.

Sourceval 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.

Notations
Sourceval (>>=) : 'a t -> ('a -> 'b t) -> 'b t

Notation for bind.

Sourceval (<*>) : unit t -> 'a t -> 'a t

Sequence.

List operations
module List : Monad.ListS with type 'a t := 'a t
Notations
Sourcemodule Notations : sig ... end