Agda.Auto.Auto

Documentation

auto :: MonadTCM tcm => InteractionId -> Range -> String -> tcm AutoResult

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

Constructors

AutoResult

Fields

• autoProgress :: AutoProgress
• autoMessage :: Maybe String

data AutoProgress

Result type: Progress & potential Message for the user

The of the Auto tactic can be one of the following three:

1. Solutions [(ii,s)] A list of solutions s for interaction ids ii. In particular, Solutions [] means Agsy found no solution.
2. FunClauses cs A list of clauses for the interaction id ii in which Auto was invoked with case-splitting turned on.
3. Refinement s A refinement for the interaction id ii in which Auto was invoked.

Constructors

Solutions [(InteractionId, String)]

FunClauses [String]

Refinement String