| Safe Haskell | Safe |
|---|---|
| Language | Haskell98 |
DDC.Source.Tetra.Transform.BoundX
Description
Lifting and lowering level-0 deBruijn indices in source expressions.
Level-0 indices are used for both value and witness variables.
- liftX :: (MapBoundX c l, GBound l ~ Bound n) => Int -> c l -> c l
- liftAtDepthX :: (MapBoundX c l, GBound l ~ Bound n) => l -> Int -> Int -> c l -> c l
- class HasAnonBind l => MapBoundX c l where
- mapBoundAtDepthX :: l -> (Int -> GBound l -> GBound l) -> Int -> c l -> c l
- class HasAnonBind l where
Documentation
liftX :: (MapBoundX c l, GBound l ~ Bound n) => Int -> c l -> c l Source
Wrapper for liftAtDepthX that starts at depth 0.
Arguments
| :: (MapBoundX c l, GBound l ~ Bound n) | |
| => 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
Instances
| HasAnonBind l => MapBoundX GWitness l Source | |
| HasAnonBind l => MapBoundX GCast l Source | |
| HasAnonBind l => MapBoundX GGuard l Source | |
| HasAnonBind l => MapBoundX GGuardedExp l Source | |
| HasAnonBind l => MapBoundX GAlt l Source | |
| HasAnonBind l => MapBoundX GClause l Source | |
| HasAnonBind l => MapBoundX GExp l Source |
class HasAnonBind l where Source
Instances
| HasAnonBind (Annot a) Source |