Safe Haskell | None |
---|
- auto :: InteractionId -> Range -> String -> TCM (Either [(InteractionId, String)] (Either [String] String), Maybe String)
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 solutionss
for 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 idii
in which Auto was invoked.