| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Auto.Auto
Synopsis
- auto :: MonadTCM tcm => InteractionId -> Range -> String -> tcm AutoResult
- data AutoResult = AutoResult {
- autoProgress :: AutoProgress
- autoMessage :: Maybe String
- data AutoProgress
- = Solutions [(InteractionId, String)]
- | FunClauses [String]
- | Refinement String
Documentation
auto :: MonadTCM tcm => InteractionId -> Range -> String -> tcm AutoResult Source #
Entry point for Auto tactic (Agsy).
If the autoMessage part of the result is set to Just msg, the
message msg produced by Agsy should be displayed to the user.
data AutoResult Source #
Constructors
| AutoResult | |
Fields
| |
data AutoProgress Source #
Result type: Progress & potential Message for the user
The of the Auto tactic can be one of the following three:
Solutions [(ii,s)]A list of solutionssfor interaction idsii. In particular,Solutions []means Agsy found no solution.FunClauses csA list of clauses for the interaction idiiin which Auto was invoked with case-splitting turned on.Refinement sA refinement for the interaction idiiin which Auto was invoked.
Constructors
| Solutions [(InteractionId, String)] | |
| FunClauses [String] | |
| Refinement String |