Agda.Interaction.MakeCase

Documentation

type CaseContext = Maybe ExtLamInfo

parseVariables

Arguments

:: QName

The function name.

-> Telescope

The telescope of the clause we are splitting.

-> InteractionId

The hole of this function we are working on.

-> Range

The range of this hole.

-> [String]

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

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

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

getClauseZipperForIP :: QName -> Int -> TCM (CaseContext, ClauseZipper)

recheckAbstractClause :: Type -> Maybe Substitution -> SpineClause -> TCM Clause

makeCase :: InteractionId -> Range -> String -> TCM (QName, CaseContext, [Clause])

Entry point for case splitting tactic.

makePatternVarsVisible :: [Nat] -> SplitClause -> SplitClause

Make the given pattern variables visible by marking their origin as CaseSplit and pattern origin as PatOSplit in the SplitClause.

makeAbsurdClause :: QName -> ExpandedEllipsis -> SplitClause -> TCM Clause

Make clause with no rhs (because of absurd match).

makeAbstractClause :: QName -> RHS -> ExpandedEllipsis -> SplitClause -> TCM Clause

Make a clause with a question mark as rhs.

anyEllipsisVar :: QName -> SpineClause -> [Name] -> TCM Bool