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

Safe HaskellSafe-Infered

DDC.Type.Transform.LowerT

Description

Lowering of deBruijn indices in a type.

Documentation

class LowerT c whereSource

Methods

lowerAtDepthTSource

Arguments

:: forall n . Ord n 
=> Int

Number of levels to lower.

-> Int

Current binding depth.

-> c n

Lower type indices in this thing.

-> c n 

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

lowerTSource

Arguments

:: forall n . Ord n 
=> Int

Number of levels to lower.

-> c n

Lower type indices in this thing.

-> c n 

Wrapper for lowerAtDepthT that starts at depth 0.