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

Safe Haskell | None
Language | Haskell2010

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 Source #

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

Methods

dropArgs :: Int -> a -> a Source #

#### Instances

Instances details

DropArgs Clause Source # | NOTE: does not work for recursive functions.
Instance details Defined in Agda.TypeChecking.DropArgs Methods dropArgs :: Int -> Clause -> Clause Source #
DropArgs Telescope Source # | NOTE: This creates telescopes with unbound de Bruijn indices.
Instance details Defined in Agda.TypeChecking.DropArgs Methods dropArgs :: Int -> Telescope -> Telescope Source #
DropArgs Term Source # | Use for dropping initial lambdas in clause bodies. NOTE: does not reduce term, need lambdas to be present.
Instance details Defined in Agda.TypeChecking.DropArgs Methods dropArgs :: Int -> Term -> Term Source #
DropArgs CompiledClauses Source # | 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.
Instance details Defined in Agda.TypeChecking.DropArgs Methods dropArgs :: Int -> CompiledClauses -> CompiledClauses Source #
DropArgs SplitTree Source # |
Instance details Defined in Agda.TypeChecking.DropArgs Methods dropArgs :: Int -> SplitTree -> SplitTree Source #
DropArgs FunctionInverse Source # |
Instance details Defined in Agda.TypeChecking.DropArgs Methods dropArgs :: Int -> FunctionInverse -> FunctionInverse Source #
DropArgs Permutation Source # |
Instance details Defined in Agda.TypeChecking.DropArgs Methods dropArgs :: Int -> Permutation -> Permutation Source #
DropArgs a => DropArgs (Maybe a) Source # |
Instance details Defined in Agda.TypeChecking.DropArgs Methods dropArgs :: Int -> Maybe a -> Maybe a Source #