| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Auto.Auto
Documentation
auto :: InteractionId -> Range -> String -> TCM (Either [(InteractionId, String)] (Either [String] String), Maybe String) Source #
Entry point for Auto tactic (Agsy).
auto ii rng s = return (res, mmsg)
If mmsg = Just msg, the message msg produced by Agsy should
be displayed to the user.
The result res of the Auto tactic can be one of the following three:
Left [(ii,s)]A list of solutionssfor interaction idsii. In particular,Left []means Agsy found no solution.Right (Left cs)A list of clauses (the user allowed case-split).Right (Right s)A refinement for the interaction idiiin which Auto was invoked.