ddc-core-0.2.1.1: Disciple Core language and type checker.

Safe HaskellSafe-Infered

DDC.Type.Transform.LiftT

Description

Lifting of deBruijn indices in a type.

Documentation

class LiftT c whereSource

Methods

liftAtDepthTSource

Arguments

:: forall n . Ord n 
=> Int

Number of levels to lift.

-> Int

Current binding depth.

-> c n

Lift type indices in this thing.

-> c n 

Lift type indices that are at least a certain depth by the given number of levels.

liftTSource

Arguments

:: forall n . Ord n 
=> Int

Number of levels to lift

-> c n

Lift type indices in this thing.

-> c n 

Wrapper for liftAtDepthT that starts at depth 0.