Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

Agda.TypeChecking.DropArgs

Contents

- Dropping initial arguments to create a projection-like function

Synopsis

- class DropArgs a where
  - dropArgs :: Int -> a -> a

# Dropping initial arguments to create a projection-like function

class DropArgs a where

When making a function projection-like, we drop the first `n` arguments.

Methods

dropArgs :: Int -> a -> a

Instances

DropArgs Permutation |
DropArgs ClauseBody | NOTE: does not go into the body, so does not work for recursive functions.
DropArgs Clause | NOTE: does not work for recursive functions.
DropArgs Telescope | NOTE: This creates telescopes with unbound de Bruijn indices.
DropArgs CompiledClauses | To drop the first `n` arguments in a compiled clause, we reduce the split argument indices by `n` and drop `n` arguments from the bodies. NOTE: this only works for non-recursive functions, we are not dropping arguments to recursive calls in bodies.
DropArgs FunctionInverse |