Generics.SOP.Dict

An explicit dictionary carrying evidence of a class constraint.

The constraint parameter is separated into a second argument so that Dict c is of the correct kind to be used directly as a parameter to e.g. NP.

The constraint All (All c) is convertible to All2 c.

The constraint All2 c is convertible to All (All c).

If we have a product containing proofs that each element of xs satisfies c, then All c holds for xs.

If we have a product of products containing proofs that each inner element of xss satisfies c, then All2 c holds for xss.

A structure of dictionaries.

Lifts a dictionary conversion over a type-level list.

Lifts a dictionary conversion over a type-level list of lists.

A proof that the trivial constraint holds over all type-level lists.

A proof that the trivial constraint holds over all type-level lists of lists.

If we have a constraint c that holds over a type-level list xs, we can create a product containing proofs that each individual list element satisfies c.

If we have a constraint c that holds over a type-level list of lists xss, we can create a product of products containing proofs that all the inner elements satisfy c.

If we have an explicit dictionary, we can unwrap it and pass a function that makes use of it.

If two constraints c and d hold over a type-level list xs, then the combination of both constraints holds over that list.

If two constraints c and d hold over a type-level list of lists xss, then the combination of both constraints holds over that list of lists.