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-3.0.0.tbz
sha256=1066aed2618fd8e6a400c5147dbf55ea977ce8d3fe2e518ac6785c6775a1b8be
sha512=f7f499626aba92e070ae69581299a58525973fdbfd04a160ed3ac89209fb6cbe307b816d0b23e1b75bc83467ce8b4b0530c6f9816eaf58f7a07fde65a450106c

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