Safe Haskell	Unsafe
Language	Haskell2010

DeBruijn.Internal.Add

Contents

Synopsis

newtype Add (n :: Ctx) (m :: Ctx) (p :: Ctx) where
- UnsafeAdd Int
- pattern AZ :: () => (n ~ EmptyCtx, m ~ p) => Add n m p
- pattern AS :: forall n p m n' p'. () => (n ~ S n', p ~ S p') => Add n' m p' -> Add n m p
addToInt :: forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Add n m p -> Int
addToSize :: forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Add n m p -> Size n
adding :: forall (n :: Ctx) (ctx :: Ctx). Size n -> Some (Add n ctx)
rzeroAdd :: forall (n :: Ctx). Size n -> Add n EmptyCtx n
unrzeroAdd :: forall (n :: Ctx) (m :: Ctx). Add n EmptyCtx m -> n :~: m
lzeroAdd :: forall (n :: Ctx). Size n -> Add EmptyCtx n n
unlzeroAdd :: forall (n :: Ctx) (m :: Ctx). Add EmptyCtx n m -> n :~: m
rsuccAdd :: forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Add n m p -> Add n (S m) (S p)
unrsuccAdd :: forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Add n (S m) (S p) -> Add n m p
lsuccAdd :: forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Add n m p -> Add (S n) m (S p)
unlsuccAdd :: forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Add (S n) m (S p) -> Add n m p
swapAdd :: forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Add n (S m) p -> Add (S n) m p
unswapAdd :: forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Add (S n) m p -> Add n (S m) p

Documentation

newtype Add (n :: Ctx) (m :: Ctx) (p :: Ctx) 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.

Constructors

Bundled Patterns

pattern AZ :: () => (n ~ EmptyCtx, m ~ p) => Add n m p
pattern AS :: forall n p m n' p'. () => (n ~ S n', p ~ S p') => Add n' m p' -> Add n m p

Instances details

GShow (Add n m :: Ctx -> Type) Source #
Instance details Defined in DeBruijn.Internal.Add Methods gshowsPrec :: forall (a :: Ctx). 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 :: forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Add n m p -> Int Source #

addToSize :: forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Add n m p -> Size n Source #

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

Add n to some context ctx.

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

Lemmas

n + 0 ≡ 0

unrzeroAdd :: forall (n :: Ctx) (m :: Ctx). Add n EmptyCtx m -> n :~: m Source #

n + 0 ≡ m → n ≡ m

0 + n ≡ 0

unlzeroAdd :: forall (n :: Ctx) (m :: Ctx). Add EmptyCtx n m -> n :~: m Source #

0 + n ≡ m → n ≡ m

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

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

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

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

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

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

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

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

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

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

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

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