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 (6)

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.3.0.tar.gz
sha256=3f0fc283e8644394aa9c7a6e3995b6d9ebbe1e6dda712bf431f9c372dcef95ad

doc/rocq-runtime.engine/Logic_monad/BackState/index.html

Module Logic_monad.BackStateSource

Sourcetype (+'a, -'i, +'o, 'e) t
Sourceval return : 'a -> ('a, 's, 's, 'e) t
Sourceval (>>=) : ('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
Sourceval 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
Sourceval plus : ('a, 'i, 'o, 'e) t -> ('e -> ('a, 'i, 'o, 'e) t) -> ('a, 'i, 'o, 'e) t
Sourceval 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
Sourceval repr : ('a, 'e) reified -> ('a, ('a, 'e) reified, 'e) list_view
Sourceval run : ('a, 'i, 'o, 'e) t -> 'i -> ('a * 'o, 'e) reified