| ||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||
| Documentation | ||||||||||||||||||||||||||||
| data Up | ||||||||||||||||||||||||||||
| data Down | ||||||||||||||||||||||||||||
| type family Invert d :: * | ||||||||||||||||||||||||||||
| data DirectionT a where | ||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||
| class Reify l a where | ||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||
| data ExistsR l r where | ||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||
| class Language l where | ||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||
| contextMovementEq :: Language l => Context l a b -> Movement l Up a c -> Maybe (TyEq b c) | ||||||||||||||||||||||||||||
| data Path l r a b where | ||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||
| foldPath :: (forall from to. Reify l to => r from to -> from -> to) -> start -> Path l r start finish -> finish | ||||||||||||||||||||||||||||
| data Cursor l x a | ||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||
| data CursorWithMovement l d x from where | ||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||
| rebuild :: Language l => Cursor l x a -> l | ||||||||||||||||||||||||||||
| applyMovement :: (Language l, Reify l a, Reify l b) => Movement l d a b -> Cursor l x a -> Maybe (Cursor l x b) | ||||||||||||||||||||||||||||
| genericMoveUp :: Language l => Cursor l x a -> Maybe (CursorWithMovement l Up x a) | ||||||||||||||||||||||||||||
| genericMoveDown :: Language l => Cursor l x a -> Maybe (CursorWithMovement l Down x a) | ||||||||||||||||||||||||||||
| genericMoveLeft :: Language l => Cursor l x a -> Maybe (ExistsR l (Cursor l x)) | ||||||||||||||||||||||||||||
| genericMoveRight :: Language l => Cursor l x a -> Maybe (ExistsR l (Cursor l x)) | ||||||||||||||||||||||||||||
| genericMoveSideways :: forall l x a. Language l => (forall a z. Movement l Down a z -> Maybe (ExistsR l (Movement l Down a))) -> Cursor l x a -> Maybe (ExistsR l (Cursor l x)) | ||||||||||||||||||||||||||||
| moveToRoot :: Language l => Cursor l x a -> Cursor l x l | ||||||||||||||||||||||||||||
| data Route l from to where | ||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||
| route_invariant :: forall l from to. Language l => Route l from to -> Bool | ||||||||||||||||||||||||||||
| updateRoute :: (Language l, Reify l a, Reify l b) => Movement l d a b -> Route l a c -> Route l b c | ||||||||||||||||||||||||||||
| resetLog :: Cursor l x a -> Cursor l a a | ||||||||||||||||||||||||||||
| appendRoute :: (Language l, Reify l a, Reify l b, Reify l c) => Route l a b -> Route l b c -> Route l a c | ||||||||||||||||||||||||||||
| followRoute :: Language l => Cursor l x a -> Route l a c -> Maybe (Cursor l x c) | ||||||||||||||||||||||||||||
| Produced by Haddock version 2.2.2 | ||||||||||||||||||||||||||||