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

Agda.Auto.Auto

Synopsis

# 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.

Constructors

 AutoResult Fields

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