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