dedukti

The Dedukti logical framework
IN THIS PACKAGE
Module Basic
type ident
val mk_ident : string -> ident
val ident_eq : ident -> ident -> bool
val string_of_ident : ident -> string
type mident
val mk_mident : string -> mident
val mident_eq : mident -> mident -> bool
val string_of_mident : mident -> string
type name
val md : name -> mident
val id : name -> ident
val mk_name : mident -> ident -> name
val name_eq : name -> name -> bool
val dmark : ident
module LList : sig ... end
type loc
val dloc : loc
val mk_loc : int -> int -> loc
val of_loc : loc -> int * int
val add_path : string -> unit
val get_path : unit -> string list
type (!'a, !'b) error =
| OK of 'a
| Err of 'b
val map_error : ( 'a -> 'b ) -> ( 'a, 'c ) error -> ( 'b, 'c ) error
val bind_error : ( 'a -> ( 'b, 'c ) error ) -> ( 'a, 'c ) error -> ( 'b, 'c ) error
val map_error_list : ( 'a -> ( 'b, 'c ) error ) -> 'a list -> ( 'b list, 'c ) error
val set_debug_mode : int -> unit
val debug : int -> ( 'a, Format.formatter, unit, unit ) format4 -> 'a
val warn : ( 'a, Format.formatter, unit, unit ) format4 -> 'a
val fold_map : ( 'b -> 'a -> 'c * 'b ) -> 'b -> 'a list -> 'c list * 'b
val bind_opt : ( 'a -> 'b option ) -> 'a option -> 'b option
val map_opt : ( 'a -> 'b ) -> 'a option -> 'b option
type !'a printer = Format.formatter -> 'a -> unit
val string_of : 'a printer -> 'a -> string
val pp_ident : ident printer
val pp_mident : mident printer
val pp_name : name printer
val pp_loc : loc printer
val pp_list : string -> 'a printer -> 'a list printer
val pp_arr : string -> 'a printer -> 'a array printer
val pp_option : string -> 'a printer -> 'a option printer