Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- nullary :: Text -> TacticsM () -> Parser (TacticsM ())
- unary_occ :: Text -> (OccName -> TacticsM ()) -> Parser (TacticsM ())
- unary_occM :: Text -> (OccName -> Parser (TacticsM ())) -> Parser (TacticsM ())
- variadic_occ :: Text -> ([OccName] -> TacticsM ()) -> Parser (TacticsM ())
- commands :: [SomeMetaprogramCommand]
- oneTactic :: Parser (TacticsM ())
- tactic :: Parser (TacticsM ())
- bindOne :: TacticsM a -> TacticsM a -> TacticsM a
- operators :: [[Operator Parser (TacticsM ())]]
- tacticProgram :: Parser (TacticsM ())
- wrapError :: String -> String
- attempt_it :: Context -> Judgement -> String -> ReaderT ParserContext IO (Either String String)
- parseMetaprogram :: Text -> ReaderT ParserContext IO (TacticsM ())
- getOccTy :: OccName -> Parser Type
- writeDocumentation :: IO ()
Documentation
tacticProgram :: Parser (TacticsM ()) Source #
attempt_it :: Context -> Judgement -> String -> ReaderT ParserContext IO (Either String String) Source #
Attempt to run a metaprogram tactic, returning the proof state, or the errors.
parseMetaprogram :: Text -> ReaderT ParserContext IO (TacticsM ()) Source #
writeDocumentation :: IO () Source #
Automatically generate the metaprogram command reference.