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

• infoTel0 :: Telescope
   
• infoTel :: Telescope
   
• infoEqTel :: Telescope
   
• infoEqLHS :: [Term]
   
• infoEqRHS :: [Term]
   
• infoRho :: PatternSubstitution
   
• infoTau :: Substitution
   
• infoLeftInv :: Substitution
   

Fields

• covSplitArg :: Arg Nat

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

• covSplitClauses :: [(SplitTag, (SplitClause, IInfo))]

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

Fields

• coverSplitTree :: SplitTree
   
• coverUsedClauses :: IntSet
   
• coverMissingClauses :: [(Telescope, [NamedArg DeBruijnPattern])]
   
• coverPatterns :: [Clause]

  The set of patterns used as cover.

• coverNoExactClauses :: IntSet