| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Ide.Plugin.Tactic.CaseSplit
Synopsis
- mkFirstAgda :: [Pat GhcPs] -> HsExpr GhcPs -> AgdaMatch
- iterateSplit :: AgdaMatch -> [AgdaMatch]
- splitToDecl :: OccName -> [AgdaMatch] -> LHsDecl GhcPs
Documentation
mkFirstAgda :: [Pat GhcPs] -> HsExpr GhcPs -> AgdaMatch Source #
Construct an AgdaMatch from patterns in scope (should be the LHS of the
match) and a body.
iterateSplit :: AgdaMatch -> [AgdaMatch] Source #
Sometimes agdaSplit exposes another opportunity to do agdaSplit. This
function runs it a few times, hoping it will find a fixpoint.