| Safe Haskell | Unsafe |
|---|---|
| Language | Haskell2010 |
DeBruijn.Internal.Add
Contents
Synopsis
- newtype 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
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.
Bundled Patterns
| 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 |
adding :: Size n -> Some (Add n ctx) Source #
Add n to some context ctx.
>>>adding (SS (SS SZ))Some 2