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

Safe HaskellNone




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