hls-tactics-plugin-0.5.1.0: Tactics plugin for Haskell Language Server
Safe HaskellNone
LanguageHaskell2010

Ide.Plugin.Tactic.Tactics

Synopsis

Documentation

assumption :: TacticsM () Source #

Use something in the hypothesis to fill the hole.

assume :: OccName -> TacticsM () Source #

Use something named in the hypothesis to fill the hole.

intros :: TacticsM () Source #

Introduce a lambda binding every variable.

destructAuto :: OccName -> TacticsM () Source #

Case split, and leave holes in the matches.

destruct :: OccName -> TacticsM () Source #

Case split, and leave holes in the matches.

homo :: OccName -> TacticsM () Source #

Case split, using the same data constructor in the matches.

destructLambdaCase :: TacticsM () Source #

LambdaCase split, and leave holes in the matches.

homoLambdaCase :: TacticsM () Source #

LambdaCase split, using the same data constructor in the matches.

split :: TacticsM () Source #

Choose between each of the goal's data constructors.

splitAuto :: TacticsM () Source #

Choose between each of the goal's data constructors. Different than split because it won't split a data con if it doesn't result in any new goals.

requireNewHoles :: TacticsM () -> TacticsM () Source #

Allow the given tactic to proceed if and only if it introduces holes that have a different goal than current goal.

splitDataCon :: DataCon -> TacticsM () Source #

Attempt to instantiate the given data constructor to solve the goal.

matching :: (Judgement -> TacticsM ()) -> TacticsM () Source #

matching f takes a function from a judgement to a Tactic, and then applies the resulting Tactic.

attemptOn :: (Judgement -> [a]) -> (a -> TacticsM ()) -> TacticsM () Source #

runTactic Source #

Arguments

:: Context 
-> Judgement 
-> TacticsM ()

Tactic to use

-> Either [TacticError] RunTacticResults 

Attempt to generate a term of the right type using in-scope bindings, and a given tactic.