ivor-0.1.8: Theorem proving library based on dependent type theory Source code Contents Index

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

auto :: Int -> Tactic split :: Tactic left :: Tactic right :: Tactic useCon :: Int -> Int -> Tactic exists :: IsTerm a => a -> Tactic isItJust :: IsTerm a => a -> Tactic

Documentation

auto Source

:: 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 :: Tactic Source

Split a goal into subgoals. Type of goal must be a one constructor family, with constructor c, then proceeds by refine c.

left :: Tactic Source

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 :: Tactic Source

Split a goal into subgoals. Type of goal must be a two constructor family, with constructors l and r, then proceeds by refine r.

useCon Source

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

exists Source

:: 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 non-inferrable argument.

isItJust :: IsTerm a => a -> Tactic Source

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