Safe Haskell | Trustworthy |
---|---|
Language | Haskell2010 |
Synopsis
- data Add n m p where
- addToInt :: Add n m p -> Int
- addToSize :: Add n m p -> Size n
- adding :: Size n -> Some (Add n ctx)
- rzeroAdd :: Size n -> Add n EmptyCtx n
- unrzeroAdd :: Add n EmptyCtx m -> n :~: m
- lzeroAdd :: Size n -> Add EmptyCtx n n
- unlzeroAdd :: Add EmptyCtx n m -> n :~: m
- rsuccAdd :: Add n m p -> Add n (S m) (S p)
- unrsuccAdd :: Add n (S m) (S p) -> Add n m p
- lsuccAdd :: Add n m p -> Add (S n) m (S p)
- unlsuccAdd :: Add (S n) m (S p) -> Add n m p
- swapAdd :: Add n (S m) p -> Add (S n) m p
- unswapAdd :: Add (S n) m p -> Add n (S m) p
Documentation
is an evidence that Add
n m pn + m = p
.
Useful when you have an arity n
thing and need to extend a context ctx
with:
.Add
n ctx ctx'
Using a type representing a graph of a type function is often more convenient than defining type-family to begin with.
pattern AZ :: () => (n ~ EmptyCtx, m ~ p) => Add n m p | |
pattern AS :: () => (n ~ S n', p ~ S p') => Add n' m p' -> Add n m p |
Instances
adding :: Size n -> Some (Add n ctx) Source #
Add n
to some context ctx
.
>>>
adding (SS (SS SZ))
Some 2