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.Coverage.SplitClause

SplitClause and CoverResult types.

  • 5 types
  • 2 values
  • PackageAgda-2.7.0.1
  • Exports7
  • LanguageHaskell2010
  • LicenceMIT
  • SourceSplitClause.hs
datadata SplitClause
#

Constructors

  • SClause
    • scTel :: Telescope

      Type of variables in scPats.

    • scPats :: [NamedArg SplitPattern]

      The patterns leading to the currently considered branch of the split tree.

    • scSubst :: Substitution' SplitPattern

      Substitution from scTel to old context. Only needed directly after split on variable: * To update scTarget * To rename other split variables when splitting on multiple variables. scSubst is not `transitive', i.e., does not record the substitution from the original context to scTel over a series of splits. It is freshly computed after each split by computeNeighborhood; also splitResult, which does not split on a variable, should reset it to the identity idS, lest it be applied to scTarget again, leading to Issue 1294.

    • scCheckpoints :: Map CheckpointId Substitution

      We need to keep track of the module parameter checkpoints for the clause for the purpose of inferring missing instance clauses.

    • scTarget :: Maybe (Dom Type)

      The type of the rhs, living in context scTel. fixTargetType computes the new scTarget by applying substitution scSubst.

Instances1PrettyTCM
  • PrettyTCM SplitClauseDefined in Agda-2.7.0.1 · Agda.TypeChecking.Coverage · orphan

    For debugging only.