package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type

The NonLogical module allows the execution of effects (including I/O) in tactics (non-logical side-effects are not discarded at failures).

The non-logical monad is a simple unit -> 'a (i/o) monad. The operations are simple wrappers around corresponding usual operations and require little documentation.

include Monad.S
include Monad.Def
type +'a t
val return : 'a -> 'a t
val (>>=) : 'a t -> ('a -> 'b t) -> 'b t
val (>>) : unit t -> 'a t -> 'a t
val map : ('a -> 'b) -> 'a t -> 'b t

The monadic laws must hold:

  • (x>>=f)>>=g = x>>=fun x' -> (f x'>>=g)
  • return a >>= f = f a
  • x>>=return = x

As well as the following identities:

  • x >> y = x >>= fun () -> y
  • map f x = x >>= fun x' -> f x'
module List : Monad.ListS with type 'a t := 'a t
val ignore : 'a t -> unit t
type 'a ref
val ref : 'a -> 'a ref t

Pervasives.(:=)

val (:=) : 'a ref -> 'a -> unit t

Pervasives.(!)

val (!) : 'a ref -> 'a t
val read_line : string t
val print_char : char -> unit t
val print_debug : Pp.t -> unit t

Loggers. The buffer is also flushed.

val print_warning : Pp.t -> unit t
val print_notice : Pp.t -> unit t
val print_info : Pp.t -> unit t
val raise : Exninfo.iexn -> 'a t

Pervasives.raise. Except that exceptions are wrapped with Exception.

val catch : 'a t -> (Exninfo.iexn -> 'a t) -> 'a t

try ... with ... but restricted to Exception.

val timeout : float -> 'a t -> 'a option t
val make : (unit -> 'a) -> 'a t

Construct a monadified side-effect. Exceptions raised by the argument are wrapped with Exception.

val run : 'a t -> 'a

run performs effects.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct