package lambdapi

You can search for identifiers within the package.

in-package search v0.2.0

Proof assistant for the λΠ-calculus modulo rewriting

Install

dune-project

Dependency

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

Authors

D

Deducteam

Maintainers

D

dedukti-dev@inria.fr

Sources

lambdapi-3.0.0.tbz

sha256=1066aed2618fd8e6a400c5147dbf55ea977ce8d3fe2e518ac6785c6775a1b8be

sha512=f7f499626aba92e070ae69581299a58525973fdbfd04a160ed3ac89209fb6cbe307b816d0b23e1b75bc83467ce8b4b0530c6f9816eaf58f7a07fde65a450106c

doc/lambdapi.common/Common/Console/index.html

Module `Common.Console`Source

Verbose level and loggers management.

Sourceval out_fmt : Format.formatter ref

out_fmt main output formatter.

Sourceval verbose : int Timed.ref

Current verbosity level.

Sourceval default_verbose : int ref

Default verbosity level (may be set with command line arguments).

Sourceval set_default_verbose : int -> unit

set_default_verbose i sets the default verbosity level to i.

Sourceval out : int -> 'a Lplib.Base.outfmt -> 'a

out lvl fmt prints an output message using the format fmt, but only if lvl is strictly greater than the current verbosity level. Note that the output channel is automatically flushed if logging modes are enabled.

Sourceval boolean_flags : (bool * bool Timed.ref) Lplib.Extra.StrMap.t ref

List of registered boolean flags, with their default values.

Sourceval register_flag : string -> bool -> bool Timed.ref

register_flag id d registers a new boolean flag named id, with default value of d. Note the name should not have been used previously.

Sourceval set_flag : string -> bool -> unit

set_flag id b sets the value of the flag named id to be b, or raises Not_found if no flag with this name was registered.

Sourceval reset_default : unit -> unit

reset_default () resets the verbosity level and the state of the loggers to their default value (configurable by the user with command line flags). The boolean flags are also reset to their default values.

Sourcemodule State : sig ... end

Module to manipulate imperative state of the typechecker.