lambdapi

Proof assistant for the λΠ-calculus modulo rewriting
package lambdapi
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library lambdapi.common
Module Common . Library . LibMap
type t

Module path mapping.

val empty : t

empty is an empty module path mapping.

exception Already_mapped

Exception raised if an attempt is made to map an already mapped module (including the root).

val set_root : string -> t -> t

set_root dir m sets the library root of m to be dir.

  • raises Already_mapped

    if library root of m is already set.

val add : Path.t -> string -> t -> t

add mp fp map extends the mapping map by associating the module path mp to the file path fp.

  • raises Already_mapped

    when mp isalready mapped in m.

exception Root_not_set

Exception raised if an attempt is made to use the get function prior to the root being set (using set_root).

val get : Path.t -> t -> string

get mp map obtains the filename corresponding to the module path mp in map (with no particular extension).

  • raises Root_not_set

    when the root of map has not been set using set_root.

val iter : ( Path.t -> string -> unit ) -> t -> unit

iter f map calls function f on every binding stored in map.

val pp : t Lplib.Base.pp

pp ppf t prints t on formatter ppf (for debug).