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 path : Common.Path.Path.t
Path of signature containing unificaton rules symbols.
val sign : Sign.t
Ghost signature holding the symbols used in unification rules.
- All signatures depend on it (dependency set in
Sig_state.create_sign
). - All signatures open it (opened in
Sig_state.of_sign
). - It is automatically loaded.
val equiv : Term.sym
Symbol "≡".
val cons : Term.sym
Symbol ";".
unpack eqs
transforms a term of the form cons (equiv t u) (cons (equiv v w) ...)
into a list [(t,u); (v,w); ...]
.
val mem : Term.sym -> bool
mem s
is true iff s
belongs to sign
.