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.Interaction.MakeCase

  • 2 types
  • 9 values
  • PackageAgda-2.7.0.1
  • Exports11
  • LanguageHaskell2010
  • LicenceMIT
  • SourceMakeCase.hs
valueparseVariables
  1. :: QName

    The function name.

  2. -> Context

    The context of the RHS of the clause we are splitting.

  3. -> [AsBinding]

    The as-bindings of the clause we are splitting

  4. -> InteractionId

    The hole of this function we are working on.

  5. -> Range

    The range of this hole.

  6. -> [String]

    The words the user entered in this hole (variable names).

  7. -> TCM [(Int, NameInScope)]

    The computed de Bruijn indices of the variables to split on, with information about whether each variable is in scope.

#

Parse variables (visible or hidden), returning their de Bruijn indices. Used in makeCase.

typetype ClauseZipper = ([Clause], Clause, [Clause])
#

Lookup the clause for an interaction point in the signature. Returns the CaseContext, the previous clauses, the clause itself, and a list of the remaining ones.

valuemakeRHSEmptyRecord :: RHS -> RHS
#

If a copattern split yields no clauses, we must be at an empty record type. In this case, replace the rhs by record{}