| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Resin.Binders.Tree.Internal
Synopsis
- data IxEq :: (k -> *) -> k -> k -> * where
- data Inject :: (k -> *) -> k -> k -> * where
- InjectRefl :: forall f a b. IxEq f a b -> Inject f a b
- CompactCompose :: forall f i j. IxEq f i i -> IxEq f j j -> Natural -> Inject f i j
- newtype Extract :: (k -> *) -> k -> k -> * where
- data TreeEq :: (k -> *) -> k -> k -> * where
- 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
Documentation
the safe subset of the api... I think
data IxEq :: (k -> *) -> k -> k -> * where Source #
Instances
| TestEquality f => TestEquality (IxEq f i :: k -> Type) Source # | |
Defined in Resin.Binders.Tree.Internal | |
data Inject :: (k -> *) -> k -> k -> * where Source #
Inject is about
Constructors
| InjectRefl :: forall f a b. IxEq f a b -> Inject f a b | |
| CompactCompose :: forall f i j. IxEq f i i -> IxEq f j j -> Natural -> Inject f i j |
data TreeEq :: (k -> *) -> k -> k -> * where Source #
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 Source #
rightExtendInject :: Inject p a b -> p c -> Inject p a c Source #
leftExtendExtract :: p a -> Extract p b c -> Extract p a c Source #