package dedukti

  1. Overview
  2. Docs
exception Not_registered_processor

raise by get_processor if the processor has not be registered

type (_, _) equal =
  1. | Refl : 'a -> ('a, 'a) equal

we used GADTs of OCaml to declare an equality type

type equality = {
  1. 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.

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