package lambdapi
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=d01e5f13db2eaba6e4fe330667149e0059d4886c651ff9d6b672db2dfc9765ed
sha512=33b68c972aca37985ed73c527076198e7d4961c7e27c89cdabfe4d1cff97cd41ccfb85ae9499eb98ad9a0aefd920bc55555df6393fc441ac2429e4d99cddafa8
doc/lambdapi.core/Core/Print/index.html
Module Core.Print
Source
Pretty-printing for the core AST.
The functions of this module are used for printing terms and other objects defined in the Term
module. This is mainly used for displaying log messages, and feedback in case of success or error while type-checking terms or testing convertibility.
Current signature state.
notation_of s
returns the notation of symbol s
or None
.
Flag for printing the domains of λ-abstractions.
Flag for printing implicit arguments.
Flag for printing the type of uninstanciated metavariables. Remark: this does not generate parsable terms; use for debug only.
Flag for printing contexts in unification problems.
Flag for printing metavariable arguments.
Exception raised when trying to convert a term into a nat.
are_quant_args args
returns true
iff args
has only one argument that is an abstraction.
The possible priority levels are `Func
(top level, including abstraction and product), `Appl
(application) and `Atom
(smallest priority).