package lambdapi
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=221dff97ab245c49b7e6480fa2a3a331ab70eb86dd5d521e2c73151029bbb787
sha512=a39961bb7f04f739660a98a52981d4793709619cd21310ca6982ba78af81ef09e01c7517ee3b8b2687b09f7d2614d878c1d69494ca6ab8ef8205d240c216ce8a
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.
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).