Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

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.

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

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

DropArgs Permutation Source # 
Instance details

Defined in Agda.TypeChecking.DropArgs

DropArgs a => DropArgs (Maybe a) Source # 
Instance details

Defined in Agda.TypeChecking.DropArgs

Methods

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