Documentation

Fields

• 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.

Fields

• covSplitArg :: Arg Nat

  De Bruijn level (counting dot patterns) of argument we split on.

• covSplitClauses :: [(SplitTag, SplitClause)]

  Covering clauses, indexed by constructor/literal these clauses share.