Resin.Binders.Tree

Documentation

the safe subset of the api... I think

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

Constructors

PolyRefl :: IxEq f i i

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

Instances

TestEquality f => TestEquality (IxEq f i :: k -> Type)

Defined in Resin.Binders.Tree.Internal

Methods

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

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

Inject is about

Constructors

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

Instances

Semigroupoid (Inject f :: k -> k -> Type)

Defined in Resin.Binders.Tree.Internal

Methods

o :: Inject f j k1 -> Inject f i j -> Inject f i k1

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

Instances

Semigroupoid (Extract f :: k -> k -> Type)

Defined in Resin.Binders.Tree.Internal

Methods

o :: Extract f j k1 -> Extract f i j -> Extract f i k1

data TreeEq :: (k -> *) -> k -> k -> * 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