
Ivor.Construction  Portability  nonportable  Stability  experimental  Maintainer  eb@dcs.stand.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  Witness
 > 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 noninferrable 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.4.2 