Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

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

- autoProgress :: AutoProgress
- autoMessage :: Maybe String

data AutoProgress Source #

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 |