Agda-2.5.3: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell2010

Agda.Interaction.MakeCase

Synopsis

Documentation

parseVariables Source #

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]) Source #

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]) Source #

Entry point for case splitting tactic.

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

Mark the variables given by the list of deBruijn indices as UserWritten in the SplitClause.

makeAbsurdClause :: QName -> SplitClause -> TCM Clause Source #

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

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

Make a clause with a question mark as rhs.