package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

The Rocq Prover -- Core Binaries and Tools

Install

Dune Dependency

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

Authors

T

The Rocq development team, INRIA, CNRS, and contributors

Maintainers

T

The Rocq development team <coqdev@inria.fr>

Sources

rocq-9.0.0.tar.gz

md5=8d522602d23e7a665631826dab9aa92b

sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be

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

Module `Proofview_monad`Source

This file defines the datatypes used as internal states by the tactic monad, and specialises the Logic_monad to these types. It should not be used directly. Consider using Proofview instead.

Traces

Sourcemodule Trace : sig ... end

State types

Sourcetype lazy_msg = unit -> Pp.t

We typically label nodes of Trace.tree with messages to print. But we don't want to compute the result.

Sourcemodule Info : sig ... end

Info trace.

module StateStore : Store.S

Sourcetype goal = Evar.t

Sourcetype goal_with_state

Sourceval drop_state : goal_with_state -> goal

Sourceval get_state : goal_with_state -> StateStore.t

Sourceval goal_with_state : goal -> StateStore.t -> goal_with_state

Sourceval with_empty_state : goal -> goal_with_state

Sourceval map_goal_with_state : (goal -> goal) -> goal_with_state -> goal_with_state

Sourcetype proofview = {

solution : Evd.evar_map;
comb : goal_with_state list;

}

Type of proof views: current evar_map together with the list of focused goals, locally shelved goals and globally shelved goals.

Instantiation of the logic monad

Sourcemodule P : sig ... end

Sourcemodule Logical : sig ... end

Lenses to access to components of the states

Sourcemodule type State = sig ... end

Sourcemodule type Reader = sig ... end

Sourcemodule type Writer = sig ... end

Sourcemodule Pv : State with type t := proofview

Lens to the proofview.

Sourcemodule Solution : State with type t := Evd.evar_map

Lens to the evar_map of the proofview.

Sourcemodule Comb : State with type t = goal_with_state list

Lens to the list of focused goals.

Sourcemodule Env : State with type t := Environ.env

Lens to the global environment.

Sourcemodule Status : Writer with type t := bool

Lens to the tactic status (true if safe, false if unsafe)

Sourcemodule InfoL : sig ... end

Lens and utilities pertaining to the info trace

On This Page

Traces
State types
Instantiation of the logic monad
Lenses to access to components of the states