Wingman.Tactics

Documentation

assumption :: TacticsM ()

Use something in the hypothesis to fill the hole.

assume :: OccName -> TacticsM ()

Use something named in the hypothesis to fill the hole.

recursion :: TacticsM ()

restrictPositionForApplication :: TacticsM () -> TacticsM () -> TacticsM ()

intros :: TacticsM ()

Introduce a lambda binding every variable.

destructAuto :: HyInfo CType -> TacticsM ()

Case split, and leave holes in the matches.

destructOrHomoAuto :: HyInfo CType -> TacticsM ()

When running auto, in order to prune the auto search tree, we try a homomorphic destruct whenever possible. If that produces any results, we can probably just prune the other side.

destruct :: HyInfo CType -> TacticsM ()

Case split, and leave holes in the matches.

homo :: HyInfo CType -> TacticsM ()

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

destructLambdaCase :: TacticsM ()

LambdaCase split, and leave holes in the matches.

homoLambdaCase :: TacticsM ()

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

apply :: HyInfo CType -> TacticsM ()

split :: TacticsM ()

Choose between each of the goal's data constructors.

splitAuto :: TacticsM ()

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.

splitSingle :: TacticsM ()

Like split, but only works if there is a single matching data constructor for the goal.

requireNewHoles :: TacticsM () -> TacticsM ()

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

splitConLike :: ConLike -> TacticsM ()

Attempt to instantiate the given ConLike to solve the goal.

INVARIANT: Assumes the given ConLike is appropriate to construct the type with.

splitDataCon :: DataCon -> TacticsM ()

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

INVARIANT: Assumes the given datacon is appropriate to construct the type with.

destructAll :: TacticsM ()

Perform a case split on each top-level argument. Used to implement the "Destruct all function arguments" action.

userSplit :: OccName -> TacticsM ()

User-facing tactic to implement "Use constructor x"

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

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

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

localTactic :: TacticsM a -> (Judgement -> Judgement) -> TacticsM a

refine :: TacticsM ()

auto' :: Int -> TacticsM ()

overFunctions :: (HyInfo CType -> TacticsM ()) -> TacticsM ()

overAlgebraicTerms :: (HyInfo CType -> TacticsM ()) -> TacticsM ()

allNames :: Judgement -> Set OccName

applyMethod :: Class -> PredType -> OccName -> TacticsM ()

applyByName :: OccName -> TacticsM ()

runTactic

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.