generics-mrsop-gdiff-0.0.1: Reimplementation of the `gdiff` algorithm for `generics-mrsop`

Safe HaskellNone
LanguageHaskell2010

Generics.MRSOP.GDiff.Util

Description

For the lack of a better name, here we put random stuff

Synopsis

Documentation

type L1 xs = IsList xs Source #

Convenient constraint synonyms

type L2 xs ys = (IsList xs, IsList ys) Source #

type L3 xs ys zs = (IsList xs, IsList ys, IsList zs) Source #

type L4 xs ys zs as = (IsList xs, IsList ys, IsList zs, IsList as) Source #

data RList :: [k] -> * where Source #

Constructors

RList :: IsList ts => RList ts 

reify :: ListPrf ts -> RList ts Source #

listPrfNP :: NP p xs -> ListPrf xs Source #

Proves that the index of a value of type NP is a list. This is useful for pattern matching on said list without having to carry the product around.

split :: ListPrf xs -> NP p (xs :++: ys) -> (NP p xs, NP p ys) Source #