| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.DropArgs
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 Permutation Source # | |
Defined in Agda.TypeChecking.DropArgs Methods dropArgs :: Int -> Permutation -> Permutation Source # | |
| DropArgs SplitTree Source # | |
| 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 Methods dropArgs :: Int -> CompiledClauses -> CompiledClauses Source # | |
| DropArgs FunctionInverse Source # | |
Defined in Agda.TypeChecking.DropArgs Methods dropArgs :: Int -> FunctionInverse -> FunctionInverse Source # | |
| DropArgs a => DropArgs (Maybe a) Source # | |