HORIZON HASKELLDocslts/ghc-9.10.xc74966e2026-09-27Search names, modules, packages, or :: a typeCtrl K

GHC 9.10.3 · lts/ghc-9.10.x · c74966e · 2026-09-27

ModuleAgda-2.7.0.1Haskell2010

Agda.TypeChecking.DropArgs

  • 1 class
  • PackageAgda-2.7.0.1
  • Exports1
  • LanguageHaskell2010
  • LicenceMIT
  • SourceDropArgs.hs

Dropping initial arguments to create a projection-like function

1 declaration
classclass DropArgs a where
#

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

Methods

Instances8DropArgs, …
  • DropArgs ClauseDefined in Agda-2.7.0.1 · Agda.TypeChecking.DropArgs

    NOTE: does not work for recursive functions.

  • DropArgs TelescopeDefined in Agda-2.7.0.1 · Agda.TypeChecking.DropArgs

    NOTE: This creates telescopes with unbound de Bruijn indices.

  • DropArgs TermDefined in Agda-2.7.0.1 · Agda.TypeChecking.DropArgs

    Use for dropping initial lambdas in clause bodies. NOTE: does not reduce term, need lambdas to be present.

  • DropArgs CompiledClausesDefined in Agda-2.7.0.1 · Agda.TypeChecking.DropArgs

    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 SplitTreeDefined in Agda-2.7.0.1 · Agda.TypeChecking.DropArgs
  • DropArgs FunctionInverseDefined in Agda-2.7.0.1 · Agda.TypeChecking.DropArgs
  • DropArgs PermutationDefined in Agda-2.7.0.1 · Agda.TypeChecking.DropArgs
  • DropArgs a => DropArgs (Maybe a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.DropArgs