ModuleAgda-2.8.0.2Haskell2010
Agda.Interaction.MakeCase
Synopsis
- type CaseContext
- value parseVariables
- type ClauseZipper
- value getClauseZipperForIP
- value recheckAbstractClause
- value makeCase
- value makePatternVarsVisible
- value makeRHSEmptyRecord
- value makeAbsurdClause
- value makeAbstractClause
- value anyEllipsisVar
- PackageAgda-2.8.0.2
- Exports11
- LanguageHaskell2010
- LicenceMIT
- SourceMakeCase.hs
parseVariables :: QNameThe function name.
-> ContextThe context of the RHS of the clause we are splitting.
-> [AsBinding]The as-bindings of the clause we are splitting
-> InteractionIdThe hole of this function we are working on.
-> RangeThe 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.
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.
Entry point for case splitting tactic.
Make the given pattern variables visible by marking their origin as CaseSplit and pattern origin as PatOSplit in the SplitClause.
If a copattern split yields no clauses, we must be at an empty record type.
In this case, replace the rhs by record{}
Make clause with no rhs (because of absurd match).
Make a clause with a question mark as rhs.