lambdapi
Proof assistant for the λΠ-calculus modulo rewriting
1024" x-on:close-sidebar="sidebar=window.innerWidth > 1024 && true">
package lambdapi
-
lambdapi.tool
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
val empty : t
empty
is an empty module path mapping.
Exception raised if an attempt is made to map an already mapped module (including the root).
set_root dir m
sets the library root of m
to be dir
.
- raises Already_mapped
if library root of
m
is already set.
add mp fp map
extends the mapping map
by associating the module path mp
to the file path fp
.
- raises Already_mapped
when
mp
isalready mapped inm
.
Exception raised if an attempt is made to use the get
function prior to the root being set (using set_root
).
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 usingset_root
.
iter f map
calls function f
on every binding stored in map
.
val pp : t Lplib.Base.pp
pp ppf t
prints t
on formatter ppf
(for debug).
ON THIS PAGE
No table of contents