| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Wingman.Metaprogramming.Parser
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 ())
- operators :: [[Operator Parser (TacticsM ())]]
- tacticProgram :: Parser (TacticsM ())
- wrapError :: String -> String
- fixErrorOffset :: RealSrcLoc -> ParseErrorBundle a b -> ParseErrorBundle a b
- attempt_it :: RealSrcLoc -> Context -> Judgement -> String -> IO (Either String String)
- parseMetaprogram :: Text -> TacticsM ()
- writeDocumentation :: IO ()
Documentation
tacticProgram :: Parser (TacticsM ()) Source #
fixErrorOffset :: RealSrcLoc -> ParseErrorBundle a b -> ParseErrorBundle a b Source #
attempt_it :: RealSrcLoc -> Context -> Judgement -> String -> IO (Either String String) Source #
Attempt to run a metaprogram tactic, returning the proof state, or the errors.
parseMetaprogram :: Text -> TacticsM () Source #
writeDocumentation :: IO () Source #
Automatically generate the metaprogram command reference.