package lambdapi

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

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (12)

Authors

  1. D
    Deducteam

Maintainers

  1. D
    dedukti-dev@inria.fr

Sources

lambdapi-2.3.0.tbz
sha256=9b13c3121ef87cf4d3311a8a1db43db4be7f0e5e2a702fdaff04a3b3c432cb31
sha512=81e0760ca77cb862a5bdb8927aa37faf7141c4e2484a8163dad0a3eaa21cc691acb5f72279c78588c085f53dde4bd35186346378feac0ab55ac06a679cf2e60f

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