debruijn-0.1: de Bruijn indices and levels
Safe HaskellTrustworthy
LanguageHaskell2010

DeBruijn.Add

Contents

Synopsis

Documentation

data Add n m p where Source #

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

Instances details
GShow (Add n m :: Ctx -> Type) Source # 
Instance details

Defined in DeBruijn.Internal.Add

Methods

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

Show (Add n m p) Source # 
Instance details

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 Source #

addToSize :: Add n m p -> Size n Source #

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

Add n to some context ctx.

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

Lemmas

rzeroAdd :: Size n -> Add n EmptyCtx n Source #

n + 0 ≡ 0

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

n + 0 ≡ m → n ≡ m

lzeroAdd :: Size n -> Add EmptyCtx n n Source #

0 + n ≡ 0

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

0 + n ≡ m → n ≡ m

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

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

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

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

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

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

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

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

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

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

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

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