Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- commandProvider :: TacticCommand -> TacticProvider
- commandTactic :: ParserContext -> TacticCommand -> Text -> IO (TacticsM ())
- tcCommandId :: TacticCommand -> CommandId
- data TacticParams = TacticParams {}
- data TacticProviderData = TacticProviderData {}
- useNameFromHypothesis :: (HyInfo CType -> TacticsM a) -> OccName -> TacticsM a
Documentation
commandProvider :: TacticCommand -> TacticProvider Source #
Mapping from tactic commands to their contextual providers. See provide
,
filterGoalType
and filterBindingType
for the nitty gritty.
commandTactic :: ParserContext -> TacticCommand -> Text -> IO (TacticsM ()) Source #
A mapping from tactic commands to actual tactics for refinery.
tcCommandId :: TacticCommand -> CommandId Source #
Construct a CommandId
data TacticParams Source #