package coq

You can search for identifiers within the package.

in-package search v0.2.0

Formal proof management system

Install

Dune Dependency

coq.inria.fr Edit opam file Versions (38)

Authors

T

The Coq development team, INRIA, CNRS, and contributors.

Maintainers

C

coqdev@inria.fr

Sources

coq-8.15.0.tar.gz

sha256=73466e61f229b23b4daffdd964be72bd7a110963b9d84bd4a86bb05c5dc19ef3

doc/coq-core.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 = Environ.env -> Evd.evar_map -> 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.

Sourcemodule 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