val log_prnt : 'a Lplib.Base.outfmt -> 'a

Current signature state.

val notation_of : Term.sym -> Sign.notation option

notation_of s returns the notation of symbol s or None.

val print_domains : bool Timed.ref

Flag for printing the domains of λ-abstractions.

val print_implicits : bool Timed.ref

Flag for printing implicit arguments.

val 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.

val print_contexts : bool Timed.ref

Flag for printing contexts in unification problems.

val uid : string Lplib.Base.pp
exception Not_a_nat

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

val nat_of_term : Term.term -> int

nat_of_term t converts a term into a natural number.

  • raises Not_a_nat

    if this is not possible.

val are_quant_args : Term.term list -> bool

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

type priority = [
| `Func
| `Appl
| `Atom

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

val prod : (Term.term * bool list) Lplib.Base.pp
val unif_rule : Term.rule Lplib.Base.pp
val rules_of : Term.sym Lplib.Base.pp
val constrs : Term.constr list Lplib.Base.pp