Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone




Dropping initial arguments to create a projection-like function

class DropArgs a whereSource

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


dropArgs :: Int -> a -> aSource


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