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]

The computed de Bruijn indices of the variables to split on.

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

getClauseForIP :: QName -> Int -> TCM (CaseContext, Clause, [Clause])

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

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 -> SplitClause -> TCM Clause

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

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

Make a clause with a question mark as rhs.