package dedukti

You can search for identifiers within the package.

in-package search v0.2.0

An implementation of The Lambda-Pi Modulo Theory

Install

sha512=97171b48dd96043d84587581d72edb442f63e7b5ac1695771aa1c3c9074739e15bc7d17678fedb7062acbf403a0bf323d97485c31b92376b80c63b5c2300ee3c

sha256=5e1b6a859dfa1eb2098947a99c7d11ee450f750d96da1720f4834e1505d1096c

Pretty printing.

Sourceval print_db_enabled : bool ref

This function is here for debug purposes. It prints terms with De Bruijn indices. The terms output this way cannot be parsed again.

Sourceval print_default_name : bool ref

Names for rules are optional. If this option is set to true, the printing functions will output default rule names given by Dedukti.

Sourceval print_module_name : bool ref

Sourcemodule type Sig = sig ... end

Sourcemodule type Printer = sig ... end

Sourcemodule Make (S : Sig) : Printer

Sourcemodule Default : Printer