package lambdapi

  1. Overview
  2. Docs
Proof assistant for the λΠ-calculus modulo rewriting

Install

Dune Dependency

Authors

Maintainers

Sources

lambdapi-2.4.1.tbz
sha256=221dff97ab245c49b7e6480fa2a3a331ab70eb86dd5d521e2c73151029bbb787
sha512=a39961bb7f04f739660a98a52981d4793709619cd21310ca6982ba78af81ef09e01c7517ee3b8b2687b09f7d2614d878c1d69494ca6ab8ef8205d240c216ce8a

doc/lambdapi.core/Core/Print/index.html

Module Core.PrintSource

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.

Sourceval log_prnt : 'a Lplib.Base.outfmt -> 'a
Sourceval sig_state : Sig_state.sig_state Timed.ref

Current signature state.

Sourceval notation_of : Term.sym -> float Sign.notation option

notation_of s returns the notation of symbol s or None.

Sourceval print_domains : bool Timed.ref

Flag for printing the domains of λ-abstractions.

Sourceval print_implicits : bool Timed.ref

Flag for printing implicit arguments.

Sourceval print_meta_types : bool Timed.ref

Flag for printing the type of uninstanciated metavariables. Remark: this does not generate parsable terms; use for debug only.

Sourceval print_contexts : bool Timed.ref

Flag for printing contexts in unification problems.

Sourceval uid : string Lplib.Base.pp
Sourceval do_not_qualify : bool Timed.ref
Sourceval without_qualifying : (unit -> 'a) -> 'a
Sourceexception Not_a_nat

Exception raised when trying to convert a term into a nat.

Sourceval nat_of_term : Term.term -> int

nat_of_term t converts a term into a natural number.

Sourceval are_quant_args : Term.term list -> bool

are_quant_args args returns true iff args has only one argument that is an abstraction.

Sourcetype priority = [
  1. | `Func
  2. | `Appl
  3. | `Atom
]

The possible priority levels are `Func (top level, including abstraction and product), `Appl (application) and `Atom (smallest priority).

Sourceval prod : (Term.term * bool list) Lplib.Base.pp
Sourceval constrs : Term.constr list Lplib.Base.pp
OCaml

Innovation. Community. Security.