package coq-core

You can search for identifiers within the package.

in-package search v0.2.0

The Coq Proof Assistant -- Core Binaries and Tools

Install

Dune Dependency

coq.inria.fr Readme Edit opam file Versions (9)

Authors

T

The Coq development team, INRIA, CNRS, and contributors

Maintainers

T

The Coq development team <coqdev@inria.fr>

Sources

coq-8.20.1.tar.gz

md5=0cfaa70f569be9494d24c829e6555d46

sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2

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 = 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