package lambdapi

  1. Overview
  2. Docs
Proof assistant for the λΠ-calculus modulo rewriting

Install

Dune Dependency

Authors

Maintainers

Sources

lambdapi-2.5.1.tbz
sha256=2c251021b6fac40c05282ca183902da5b1008e69d9179d7a9543905c2c21a28a
sha512=69535f92766e6fedc2675fc214f0fb699bde2a06aa91d338c93c99756235a293cf16776f6328973dda07cf2ad402e58fe3104a08f1a896990c1778b42f7f9fcf

doc/lambdapi.common/Common/Library/LibMap/index.html

Module Library.LibMapSource

Representation of the mapping from module paths to files.

Sourcetype t

Module path mapping.

Sourceval empty : t

empty is an empty module path mapping.

Sourceexception Already_mapped

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

Sourceval set_root : string -> t -> t

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

Sourceval 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.

Sourceexception Root_not_set

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

Sourceval 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.

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

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

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

OCaml

Innovation. Community. Security.