Safe Haskell | Safe-Inferred |
---|

Lift deBruijn indices in witnesses.

# Documentation

:: 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

:: 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.