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/Logic_monad/BackState/index.html

Module `Logic_monad.BackState`Source

Sourcetype (+'a, -'i, +'o, 'e) t

Sourceval return : 'a -> ('a, 's, 's, 'e) t

Source

val (>>=) : 
  ('a, 'i, 'm, 'e) t ->
  ('a -> ('b, 'm, 'o, 'e) t) ->
  ('b, 'i, 'o, 'e) t

Sourceval (>>) : (unit, 'i, 'm, 'e) t -> ('b, 'm, 'o, 'e) t -> ('b, 'i, 'o, 'e) t

Sourceval map : ('a -> 'b) -> ('a, 'i, 'o, 'e) t -> ('b, 'i, 'o, 'e) t

Sourceval ignore : ('a, 'i, 'o, 'e) t -> (unit, 'i, 'o, 'e) t

Sourceval set : 'o -> (unit, 'i, 'o, 'e) t

Sourceval get : ('s, 's, 's, 'e) t

Sourceval modify : ('i -> 'o) -> (unit, 'i, 'o, 'e) t

Source

val interleave : 
  ('e1 -> 'e2) ->
  ('e2 -> 'e1) ->
  ('a, 'i, 'o, 'e1) t ->
  ('a, 'i, 'o, 'e2) t

interleave src dst m adapts the exceptional content of the monad according to the functions src and dst. To ensure a meaningful result, those functions must form a retraction, i.e. dst (src e1) = e1 for all e1. This is typically the case when the type 'e1 is unit.

Sourceval zero : 'e -> ('a, 'i, 'o, 'e) t

Source

val plus : 
  ('a, 'i, 'o, 'e) t ->
  ('e -> ('a, 'i, 'o, 'e) t) ->
  ('a, 'i, 'o, 'e) t

Source

val split : 
  ('a, 's, 's, 'e) t ->
  (('a, ('a, 'i, 's, 'e) t, 'e) list_view, 's, 's, 'e) t

Sourceval once : ('a, 'i, 'o, 'e) t -> ('a, 'i, 'o, 'e) t

Sourceval break : ('e -> 'e option) -> ('a, 'i, 'o, 'e) t -> ('a, 'i, 'o, 'e) t

Sourceval lift : 'a NonLogical.t -> ('a, 's, 's, 'e) t

Sourcetype ('a, 'e) reified

Sourcetype ('a, 'e) reified_

Source

val repr : 
  ('a, 'e) reified ->
  ('a, ('a, 'e) reified_, 'e) list_view_ NonLogical.t

Sourceval run : ('a, 'i, 'o, 'e) t -> 'i -> ('a * 'o, 'e) reified

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.engine/Logic_monad/BackState/index.html

Module Logic_monad.BackStateSource

Module `Logic_monad.BackState`Source