hls-tactics-plugin-1.4.0.0: Wingman plugin for Haskell Language Server
Safe HaskellNone
LanguageHaskell2010

Wingman.CaseSplit

Synopsis

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.

splitToDecl Source #

Arguments

:: Maybe LexicalFixity 
-> OccName

The name of the function

-> [AgdaMatch] 
-> LHsDecl GhcPs 

Construct an HsDecl from a set of AgdaMatches.