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.6.0.tbz
sha256=d01e5f13db2eaba6e4fe330667149e0059d4886c651ff9d6b672db2dfc9765ed
sha512=33b68c972aca37985ed73c527076198e7d4961c7e27c89cdabfe4d1cff97cd41ccfb85ae9499eb98ad9a0aefd920bc55555df6393fc441ac2429e4d99cddafa8

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