Resin.Binders.Tree.Internal

Synopsis

• data IxEq :: (k -> Type) -> k -> k -> Type where
  • PolyRefl :: IxEq f i i
  • MonoRefl :: forall f i. f i -> IxEq f i i
• data Inject :: (k -> Type) -> k -> k -> Type 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 -> Type) -> k -> k -> Type where
  • Dual :: Inject f b a -> Extract f a b
• 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