Resin.Binders.Tree

Documentation

the safe subset of the api... I think

data IxEq :: (k -> Type) -> k -> k -> Type where

Constructors

PolyRefl :: IxEq f i i

MonoRefl :: forall f i. f i -> IxEq f i i

Instances

TestEquality k f => TestEquality k (IxEq k f i)

Methods

testEquality :: f a -> f b -> Maybe ((IxEq k f i :~: a) b)

data Inject :: (k -> Type) -> k -> k -> Type where

Inject is about

Constructors

InjectRefl :: forall f a b. IxEq f a b -> Inject f a b

Instances

Semigroupoid k (Inject k f)

Methods

o :: c j k1 -> c i j -> c i k1

data Extract :: (k -> Type) -> k -> k -> Type

Instances

Semigroupoid k (Extract k f)

Methods

o :: c j k1 -> c i j -> c i k1

data TreeEq :: (k -> Type) -> k -> k -> Type where

Constructors

TreeInject :: Inject f a b -> TreeEq f a b

TreeExtract :: Extract f a b -> TreeEq f a b

TreeRefl :: TreeEq f c c

treeElimination :: TestEquality f => Inject f a b -> Extract f b c -> TreeEq f a c

rightExtendInject :: Inject p a b -> p c -> Inject p a c

leftExtendExtract :: p a -> Extract p b c -> Extract p a c

jumpDepthInject :: Natural -> p c -> Inject p a b -> Inject p a c

jumpDepthExtract :: Natural -> Extract p b c -> p a -> Extract p a c