lambdapi

Proof assistant for the λΠ-calculus modulo rewriting
package lambdapi
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library lambdapi.lplib
Module Lplib . Base
type 'a pp = Format.formatter -> 'a -> unit

Type of pretty-printing functions.

type 'a outfmt = ( 'a, Format.formatter, unit ) format

Short name for a standard formatter.

type ('a, 'b) koutfmt = ( 'a, Format.formatter, unit, unit, unit, 'b ) format6

Short name for a standard formatter with continuation.

val out : Format.formatter -> ( 'a, Format.formatter, unit ) format -> 'a
val (++) : 'a pp -> 'b pp -> ('a0 * 'b0) pp
val (|+) : unit pp -> 'a pp -> 'a0 pp
val (+|) : 'a pp -> unit pp -> 'a0 pp
val int : int pp
val string : string pp
val unit : unit outfmt -> unit pp
val sep : string -> unit pp
val pp_if : bool -> 'a pp -> 'a pp
val prefix : string -> 'a pp -> 'a pp
val suffix : 'a pp -> string -> 'a pp
type 'a cmp = 'a -> 'a -> int

Type of comparison functions.

val cmp_map : 'b cmp -> ( 'a -> 'b ) -> 'a cmp

Comparison function through a map.

val cmp_tag : 'a cmp

Tag comparison function.

val lex : 'a cmp -> 'b cmp -> ('a * 'b) cmp

Lexicographic comparison.

val lex3 : 'a cmp -> 'b cmp -> 'c cmp -> ('a * 'b * 'c) cmp
type 'a eq = 'a -> 'a -> bool

Type of equality functions.

val eq_of_cmp : 'a cmp -> 'a eq
module Int : sig ... end