ivor-0.1.11: Theorem proving library based on dependent type theorySource codeContentsIndex
Ivor.Construction
Portabilitynon-portable
Stabilityexperimental
Maintainereb@dcs.st-and.ac.uk
Description
Some generic tactics for solving goals by applying constructors
Synopsis
auto :: Int -> Tactic
split :: Tactic
left :: Tactic
right :: Tactic
useCon :: Int -> Int -> Tactic
exists :: IsTerm a => a -> Tactic
isItJust :: IsTerm a => a -> Tactic
Documentation
autoSource
:: IntSearch 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 :: TacticSource
Split a goal into subgoals. Type of goal must be a one constructor family, with constructor c, then proceeds by refine c.
left :: TacticSource
Split a goal into subgoals. Type of goal must be a two constructor family, with constructors l and r, then proceeds by refine l.
right :: TacticSource
Split a goal into subgoals. Type of goal must be a two constructor family, with constructors l and r, then proceeds by refine r.
useConSource
:: IntEnsure at least this number of constructors (0 for no constraint)
-> IntUse this constructor (0 based, order of definition)
-> Tactic
Solve the goal by applying a numbered constructor
existsSource
:: 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.
isItJust :: IsTerm a => a -> TacticSource
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