|
Ivor.Construction | Portability | non-portable | Stability | experimental | Maintainer | eb@dcs.st-and.ac.uk |
|
|
|
Description |
Some generic tactics for solving goals by applying constructors
|
|
Synopsis |
|
|
|
Documentation |
|
|
:: Int | Search depth
| -> Tactic | | Tries to solve a simple goal automatically by trying each of these
in turn:
* Looking for an assumption (trivial)
* intros everything then solve by auto
* Splitting the goal, then solving each subgoal by auto
* If the goal is of a type with more than one constructor, try auto
on each constructor in turn.
FIXME: not that this actually works yet.
|
|
|
|
Split a goal into subgoals. Type of goal must be a one constructor
family, with constructor c, then proceeds by refine c.
|
|
|
Split a goal into subgoals. Type of goal must be a two constructor
family, with constructors l and r, then proceeds by refine l.
|
|
|
Split a goal into subgoals. Type of goal must be a two constructor
family, with constructors l and r, then proceeds by refine r.
|
|
|
:: Int | Ensure at least this number of constructors (0 for no constraint)
| -> Int | Use this constructor (0 based, order of definition)
| -> Tactic | | Solve the goal by applying a numbered constructor
|
|
|
|
:: IsTerm a | | => a | | -> Tactic | | Solve an existential by providing a witness.
More generally; apply the first constructor of the
goal's type and provide the witness as its first non-inferrable argument.
|
|
|
|
Try to solve a goal A by evaluating a term of type Maybe A. If the
answer is Just a, fill in the goal with the proof term a.
|
|
Produced by Haddock version 2.6.0 |