| Safe Haskell | Trustworthy |
|---|---|
| Language | Haskell2010 |
Resin.Binders.Tree
- data IxEq :: (k -> Type) -> k -> k -> Type where
- data Inject :: (k -> Type) -> k -> k -> Type where
- InjectRefl :: forall f a b. IxEq f a b -> Inject f a b
- data Extract :: (k -> Type) -> k -> k -> Type
- data TreeEq :: (k -> Type) -> k -> k -> Type 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 -> Type) -> k -> k -> Type where Source #
Instances
| TestEquality k f => TestEquality k (IxEq k f i) Source # | |
data Inject :: (k -> Type) -> k -> k -> Type where Source #
Inject is about
Constructors
| InjectRefl :: forall f a b. IxEq f a b -> Inject f a b |
Instances
| Semigroupoid k (Inject k f) Source # | |
data Extract :: (k -> Type) -> k -> k -> Type Source #
Instances
| Semigroupoid k (Extract k f) Source # | |
data TreeEq :: (k -> Type) -> k -> k -> Type 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 #