package lambdapi
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=2c251021b6fac40c05282ca183902da5b1008e69d9179d7a9543905c2c21a28a
sha512=69535f92766e6fedc2675fc214f0fb699bde2a06aa91d338c93c99756235a293cf16776f6328973dda07cf2ad402e58fe3104a08f1a896990c1778b42f7f9fcf
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).