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.5.0.tbz
sha256=9bc8ae3694dd51bd5742e7aba760bd2878c4b0e5ef9b3d4a7b06f3cd303b611d
sha512=c812c3129b3d85b0c4d7e741d11137dbb4fe2a0aaba3a5968409080b742924ecb506280c19ad83ef6bc910346db96d87780313fa7683c29345edae16ae79c704

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