Safe Haskell | None |
---|---|
Language | Haskell98 |
Lifting level-0 deBruijn indices in source expressions.
Level-0 indices are used for both value and witness variables.
- liftX :: (MapBoundX c l, GXBoundVar l ~ Bound) => Int -> c l -> c l
- liftAtDepthX :: (MapBoundX c l, GXBoundVar l ~ Bound) => l -> Int -> Int -> c l -> c l
- class HasAnonBind l => MapBoundX c l where
- class HasAnonBind l where
Documentation
liftX :: (MapBoundX c l, GXBoundVar l ~ Bound) => Int -> c l -> c l Source #
Wrapper for liftAtDepthX
that starts at depth 0.
:: (MapBoundX c l, GXBoundVar l ~ Bound) | |
=> l | |
-> Int | Number of levels to lift. |
-> Int | Current binding depth. |
-> c l | Lift expression indices in this thing. |
-> c l |
Lift debruijn indices less than or equal to the given depth.
class HasAnonBind l => MapBoundX c l where Source #
mapBoundAtDepthX :: l -> (Int -> GXBoundVar l -> GXBoundVar l) -> Int -> c l -> c l Source #
HasAnonBind l => MapBoundX GWitness l Source # | |
HasAnonBind l => MapBoundX GCast l Source # | |
HasAnonBind l => MapBoundX GAltMatch l Source # | |
HasAnonBind l => MapBoundX GAltCase l Source # | |
HasAnonBind l => MapBoundX GGuard l Source # | |
HasAnonBind l => MapBoundX GGuardedExp l Source # | |
HasAnonBind l => MapBoundX GClause l Source # | |
HasAnonBind l => MapBoundX GExp l Source # | |