package lambdapi

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

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (12)

Authors

  1. D
    Deducteam

Maintainers

  1. D
    dedukti-dev@inria.fr

Sources

lambdapi-3.0.0.tbz
sha256=1066aed2618fd8e6a400c5147dbf55ea977ce8d3fe2e518ac6785c6775a1b8be
sha512=f7f499626aba92e070ae69581299a58525973fdbfd04a160ed3ac89209fb6cbe307b816d0b23e1b75bc83467ce8b4b0530c6f9816eaf58f7a07fde65a450106c

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 : 'a Lplib.Base.outfmt -> 'a
Sourceval sig_state : Sig_state.sig_state Timed.ref

Current signature state.

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 print_meta_args : bool Timed.ref

Flag for printing metavariable arguments.

Sourceval safe_unbind_no_check : int Lplib.Extra.StrMap.t -> Term.binder -> (Term.var * Term.term) * int Lplib.Extra.StrMap.t
Sourceval uid : string Lplib.Base.pp
Sourceval do_not_qualify : bool Timed.ref
Sourceval no_qualif : (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 pos_of_term : Term.term -> int

pos_of_term t converts a term into a positive number.

Sourceval int_of_term : Term.term -> int

int_of_term t converts a term into a positive 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 pp : [> `Appl | `Atom | `Func ] -> int Lplib.Extra.StrMap.t -> Format.formatter -> Term.term -> unit
Sourceval quantifier : int Lplib.Extra.StrMap.t -> Format.formatter -> Term.sym -> Term.term list -> unit
Sourceval head : int Lplib.Extra.StrMap.t -> bool -> Format.formatter -> Term.term -> unit
Sourceval abstractions : int Lplib.Extra.StrMap.t -> Format.formatter -> Term.term -> unit
Sourceval env : Format.formatter -> Term.term array -> unit
Sourceval prod_in : int Lplib.Extra.StrMap.t -> (Term.term * bool list) Lplib.Base.pp
Sourceval prod : (Term.term * bool list) Lplib.Base.pp
Sourceval sym_type : Format.formatter -> Term.sym -> unit
Sourceval constrs : Term.constr list Lplib.Base.pp