Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- assumption :: TacticsM ()
- assume :: OccName -> TacticsM ()
- recursion :: TacticsM ()
- intros :: TacticsM ()
- destructAuto :: OccName -> TacticsM ()
- destruct :: OccName -> TacticsM ()
- homo :: OccName -> TacticsM ()
- destructLambdaCase :: TacticsM ()
- homoLambdaCase :: TacticsM ()
- apply :: OccName -> TacticsM ()
- split :: TacticsM ()
- splitAuto :: TacticsM ()
- requireNewHoles :: TacticsM () -> TacticsM ()
- splitDataCon :: DataCon -> TacticsM ()
- matching :: (Judgement -> TacticsM ()) -> TacticsM ()
- attemptOn :: (Judgement -> [a]) -> (a -> TacticsM ()) -> TacticsM ()
- localTactic :: TacticsM a -> (Judgement -> Judgement) -> TacticsM a
- auto' :: Int -> TacticsM ()
- overFunctions :: (OccName -> TacticsM ()) -> TacticsM ()
- overAlgebraicTerms :: (OccName -> TacticsM ()) -> TacticsM ()
- allNames :: Judgement -> [OccName]
- runTactic :: Context -> Judgement -> TacticsM () -> Either [TacticError] RunTacticResults
Documentation
assumption :: TacticsM () Source #
Use something in the hypothesis to fill the hole.
destructAuto :: OccName -> TacticsM () Source #
Case split, and leave holes 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.
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
.
:: 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.