Documentation

Instances of the NuMatching a class allow pattern-matching on multi-bindings whose bodies have type a, i.e., on multi-bindings of type Mb ctx a. The structure of this class is mostly hidden from the user; see mkNuMatching to see how to create instances of the NuMatching class.

Template Haskell function for creating NuMatching instances for (G)ADTs. Typical usage is to include the following line in the source file for (G)ADT T (here assumed to have two type arguments):

$(mkNuMatching [t| forall a b . T a b |])

The mkNuMatching call here will create an instance declaration for NuMatching (T a b). It is also possible to include a context in the forall type; for example, if we define the ID data type as follows:

data ID a = ID a

then we can create a NuMatching instance for it like this:

$( mkNuMatching [t| NuMatching a => ID a |])

Note that, when a context is included, the Haskell parser will add the forall a for you.

This type states that it is possible to replace free names with fresh names in an object of type a. This type essentially just captures a representation of the type a as either a Name type, a multi-binding, a function type, or a (G)ADT. In order to be sure that only the "right" proofs are used for (G)ADTs, however, this type is hidden from the user, and can only be constructed with mkNuMatching.

Build an MbTypeRepr for type a by using an isomorphism with an already-representable type b. This is useful for building NuMatching instances for, e.g., Integral types, by mapping to and from Integer, without having to define instances for each one in this module.