DeBruijn.Add

Documentation

data Add n m p where

Add n m p is an evidence that n + 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

Instances

GShow (Add n m :: Ctx -> Type)

Defined in DeBruijn.Internal.Add

Methods

gshowsPrec :: forall (a :: k). Int -> Add n m a -> ShowS

Show (Add n m p)

Defined in DeBruijn.Internal.Add

Methods

showsPrec :: Int -> Add n m p -> ShowS

show :: Add n m p -> String

showList :: [Add n m p] -> ShowS

addToInt :: Add n m p -> Int

addToSize :: Add n m p -> Size n

adding :: Size n -> Some (Add n ctx)

Add n to some context ctx.

>>> adding (SS (SS SZ))
Some 2

Lemmas

rzeroAdd :: Size n -> Add n EmptyCtx n

n + 0 ≡ 0

unrzeroAdd :: Add n EmptyCtx m -> n :~: m

n + 0 ≡ m → n ≡ m

lzeroAdd :: Size n -> Add EmptyCtx n n

0 + n ≡ 0

unlzeroAdd :: Add EmptyCtx n m -> n :~: m

0 + n ≡ m → n ≡ m

rsuccAdd :: Add n m p -> Add n (S m) (S p)

n + m ≡ p → n + S m ≡ S p

unrsuccAdd :: Add n (S m) (S p) -> Add n m p

n + S m ≡ S p → n + m ≡ p

lsuccAdd :: Add n m p -> Add (S n) m (S p)

n + m ≡ p → S n + m ≡ S p

unlsuccAdd :: Add (S n) m (S p) -> Add n m p

S n + m ≡ S p → n + m ≡ p

swapAdd :: Add n (S m) p -> Add (S n) m p

n + S m ≡ p → S n + m ≡ p

unswapAdd :: Add (S n) m p -> Add n (S m) p

S n + m ≡ p → n + S m ≡ p