This library provides an interface for writing tactics for Agda. It also provides several basic tactics and tactic combinators.
Currently the following tactics are supported:
- exact: solve a goal with an explicitly given value
- admit: solve a goal by creating a new postulate
- assumption: search the context for a variable that fits the goal
- intro: refine the goal by introducing a lambda
- intros: refine the goal by introducing as many lambdas as possible
- introAbsurd: solve the goal with an absurd lambda
- introConstructor: refine the goal by introducing a constructor that fits the hole
- introConstructors: refine the goal by repeatedly introducing constructors that fit the (sub)goals
- refine: refine the goal with a given term applied to some arguments
- mini-auto: repeatedly apply assumption, intro, and introConstructor
- mini-auto-with: repeatedly apply assumption, intro, introConstructor, and refine with terms from a given list of hints
- destruct: case split on the given variable (using a pattern-matching lambda)
The library is currently still work in progress and anything is subject to change at any time.