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

Safe HaskellSafe-Inferred

DDC.Core.Transform.LiftW

Description

Lift deBruijn indices in witnesses.

Documentation

class LiftW c whereSource

Methods

liftAtDepthWSource

Arguments

:: forall n . Ord n 
=> Int

Number of levels to lift.

-> Int

Current binding depth.

-> c n

Lift witness variable indices in this thing.

-> c n 

Lift indices that are at least a the given depth by some number of levels

liftWSource

Arguments

:: forall n . Ord n 
=> Int

Number of levels to lift.

-> c n

Lift witness variable indices in this thing.

-> c n 

Wrapper for liftAtDepthX that starts at depth 0.