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

Dune Dependency

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

Authors

D

dedukti-dev@inria.fr

Maintainers

D

dedukti-dev@inria.fr

Sources

v2.7.tar.gz

sha512=97171b48dd96043d84587581d72edb442f63e7b5ac1695771aa1c3c9074739e15bc7d17678fedb7062acbf403a0bf323d97485c31b92376b80c63b5c2300ee3c

sha256=5e1b6a859dfa1eb2098947a99c7d11ee450f750d96da1720f4834e1505d1096c

doc/dedukti.api/Api/Processor/Registration/index.html

Module `Processor.Registration`Source

Sourceexception Not_registered_processor

raise by get_processor if the processor has not be registered

Sourcetype (_, _) equal =

| Refl : 'a -> ('a, 'a) equal

we used GADTs of OCaml to declare an equality type

Sourcetype equality = {

equal : 'a 'b. ('a t * 'b t) -> ('a t, 'b t) equal option;

}

This record uses polymorism of rank 2. This is because internally we need to compare values of types 'a t and 'b t. Hence the "for all quantifier" on types cannot be in prenex form in the function register_processor. We use the GADT above to keep track of the dependency.

Source

val register_processor : 
  'a t ->
  equality ->
  (module S with type t = 'a) ->
  unit

register_processor processor f_eq (module P) associate the [processor] to the module [P]. ASSERT: f_eq processor processor = (Some Refl processor) ASSERT: f_eq _ _ = None