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

Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.DropArgs

Contents

Synopsis

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.

Minimal complete definition

dropArgs

Methods

dropArgs :: Int -> a -> a #

Instances

DropArgs Permutation # 
DropArgs Clause #

NOTE: does not work for recursive functions.

Methods

dropArgs :: Int -> Clause -> Clause #

DropArgs Telescope #

NOTE: This creates telescopes with unbound de Bruijn indices.

Methods

dropArgs :: Int -> Telescope -> Telescope #

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 # 
DropArgs a => DropArgs (Maybe a) # 

Methods

dropArgs :: Int -> Maybe a -> Maybe a #