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

Agda.TypeChecking.DropArgs

Synopsis

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

Minimal complete definition

dropArgs

Methods

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

Instances

 Source # Methods Source # NOTE: does not go into the body, so does not work for recursive functions. Methods Source # NOTE: does not work for recursive functions. Methods Source # NOTE: This creates telescopes with unbound de Bruijn indices. Methods 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. Methods Source # Methods DropArgs a => DropArgs (Maybe a) Source # MethodsdropArgs :: Int -> Maybe a -> Maybe a Source #