| ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

Description | ||||||||||||||||

Public interface for theorem proving gadgets. | ||||||||||||||||

Synopsis | ||||||||||||||||

System state | ||||||||||||||||

| ||||||||||||||||

Initialise a context, with no data or definitions and an empty proof state. | ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

Quickly convert a ViewTerm into a real Term.
This is dangerous; you must know that typechecking will succeed,
and the resulting term won't have a valid type, but you will be
able to run it. This is useful if you simply want to do a substitution
into a ViewTerm.
| ||||||||||||||||

| ||||||||||||||||

Check a term in the context of the given goal | ||||||||||||||||

| ||||||||||||||||

Check whether the conversion relation holds between two terms, in the context of the given goal | ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

Exported view of terms | ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

Definitions and Theorems | ||||||||||||||||

| ||||||||||||||||

Add a new definition to the global state. | ||||||||||||||||

| ||||||||||||||||

Add a new definition, with its type to the global state. These definitions can be recursive, so use with care. | ||||||||||||||||

| ||||||||||||||||

Add a new axiom to the global state. | ||||||||||||||||

| ||||||||||||||||

Declare a name which is to be defined later | ||||||||||||||||

| ||||||||||||||||

Declare a type constructor which is to be defined later | ||||||||||||||||

| ||||||||||||||||

Begin a new proof. | ||||||||||||||||

| ||||||||||||||||

Begin a new interactive definition.
Actually, just the same as theorem but this version allows you to
make recursive calls, which should of course be done with care.
| ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

Add a new binary operator on constants. Warning: The type you give is not checked! | ||||||||||||||||

| ||||||||||||||||

Add a new binary function on constants. Warning: The type you give is not checked! | ||||||||||||||||

| ||||||||||||||||

Add a new primitive function on constants, usually used for converting to some form which can be examined in the type theory itself. Warning: The type you give is not checked! | ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

Forget a definition and all following definitions. | ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

Add implicit binders for names used in a type, but not declared. |Returns the new type and the number of implicit names bound. | ||||||||||||||||

Pattern matching definitions | ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

Manipulating Proof State | ||||||||||||||||

| ||||||||||||||||

Return whether we are in the middle of proving something. | ||||||||||||||||

| ||||||||||||||||

Get the number of unsolved goals | ||||||||||||||||

| ||||||||||||||||

Suspend the current proof. Clears the current proof state; use resume
to continue the proof.
| ||||||||||||||||

| ||||||||||||||||

Resume an unfinished proof, suspending the current one if necessary.
Fails if there is no such name. Can also be used to begin a
proof of an identifier previously claimed as an axiom.
Remember that you will need to attack the goal if you are resuming an
axiom.
| ||||||||||||||||

| ||||||||||||||||

Save the state (e.g. for Undo) | ||||||||||||||||

| ||||||||||||||||

Restore a saved state; fails if none have been saved. | ||||||||||||||||

| ||||||||||||||||

Clears the saved state (e.g. if undo no longer makes sense, like when a proof has been completed) | ||||||||||||||||

| ||||||||||||||||

Get the current proof term, if we are in the middle of a proof. | ||||||||||||||||

| ||||||||||||||||

Get the goals still to be solved. | ||||||||||||||||

| ||||||||||||||||

Get the type and context of the given goal, if it exists | ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

Return whether all goals have been solved. | ||||||||||||||||

| ||||||||||||||||

Lift a finished proof into the context | ||||||||||||||||

Examining the Context | ||||||||||||||||

| ||||||||||||||||

Normalise a term and its type (using old evaluator_ | ||||||||||||||||

| ||||||||||||||||

Reduce a term and its type to Weak Head Normal Form | ||||||||||||||||

| ||||||||||||||||

Reduce a term and its type to Normal Form (using new evaluator) | ||||||||||||||||

| ||||||||||||||||

Evaluate a term in the context of the given goal | ||||||||||||||||

| ||||||||||||||||

Lookup a definition in the context. | ||||||||||||||||

| ||||||||||||||||

Check whether a name is defined | ||||||||||||||||

| ||||||||||||||||

Lookup a pattern matching definition in the context. Return the type and the pattern definition. | ||||||||||||||||

| ||||||||||||||||

Get all the names and types in the context | ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

Get all the pattern matching definitions in the context. Also returns CAFs (i.e. 0 argument functions) | ||||||||||||||||

| ||||||||||||||||

Get the names of all of the constructors of an inductive family | ||||||||||||||||

| ||||||||||||||||

Return the data type with the given name. Note that this knows nothing about the difference between parameters and indices; that information is discarded after the elimination rule is constructed. | ||||||||||||||||

| ||||||||||||||||

Get all the inductive type definitions in the context. | ||||||||||||||||

| ||||||||||||||||

Get the type of a definition in the context. | ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

Find out what type of variable the given name is | ||||||||||||||||

| ||||||||||||||||

Get an integer tag for a constructor. Each constructor has a tag unique within the data type, which could be used by a compiler. | ||||||||||||||||

| ||||||||||||||||

Get the arity of the given constructor. | ||||||||||||||||

| ||||||||||||||||

Freeze a name (i.e., set it so that it does not reduce) Fails if the name does not exist. | ||||||||||||||||

| ||||||||||||||||

Unfreeze a name (i.e., allow it to reduce). Fails if the name does not exist. | ||||||||||||||||

Goals, tactic types | ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

A tactic is any function which manipulates a term at the given goal binding. Tactics may fail, hence the monad. | ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

Get the premises of the goal | ||||||||||||||||

| ||||||||||||||||

Get the name of the goal | ||||||||||||||||

| ||||||||||||||||

Get the type of the goal | ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

Get the names and types of all goals | ||||||||||||||||

Primitive Tactics | ||||||||||||||||

Basics | ||||||||||||||||

| ||||||||||||||||

Introduce an assumption (i.e. a lambda binding) | ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

Keep introducing things until there's nothing left to introduce. | ||||||||||||||||

| ||||||||||||||||

Keep introducing things until there's nothing left to introduce, Must introduce at least one thing. | ||||||||||||||||

| ||||||||||||||||

As intros, but with names, and stop when we've run out of names.
Fails if too many names are given.
| ||||||||||||||||

| ||||||||||||||||

Add a new top level argument after the arguments its type depends on (changing the type of the theorem). This can be useful if, for example, you find you need an extra premise to prove a goal. | ||||||||||||||||

| ||||||||||||||||

Abstract over the given term in the goal. | ||||||||||||||||

| ||||||||||||||||

Abstract over the given term in the goal, and also all variables appearing in the goal whose types depend on it. | ||||||||||||||||

| ||||||||||||||||

Make a local claim | ||||||||||||||||

Proof navigation | ||||||||||||||||

| ||||||||||||||||

Focus on a different hole, i.e. set the default goal. | ||||||||||||||||

| ||||||||||||||||

Rename the outermost binder in the given goal | ||||||||||||||||

| ||||||||||||||||

Prepare a goal for introduction. | ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

Finalise a goal's solution. | ||||||||||||||||

| ||||||||||||||||

If the goal has a solution, finalise it, otherwise prepare the goal (with attack). Typically, could be used on the subgoals generated by refinement, where some may have solutions attached already, and others will need to be prepared. | ||||||||||||||||

| ||||||||||||||||

Finalise as many solutions of as many goals as possible. | ||||||||||||||||

| ||||||||||||||||

Remove a solution from a goal. | ||||||||||||||||

| ||||||||||||||||

Hide a premise | ||||||||||||||||

Introductions | ||||||||||||||||

| ||||||||||||||||

Attach a solution to a goal. | ||||||||||||||||

| ||||||||||||||||

Solve a goal by applying a function.
If the term given has arguments, attempts to fill in these arguments
by unification and solves them (with solve).
See refineWith and basicRefine for slight variations.
| ||||||||||||||||

| ||||||||||||||||

Solve a goal by applying a function.
If the term given has arguments, this will create a subgoal for each.
Some arguments may be solved by unification, in which case they will
already have a guess attached after refinement, but the guess will not
be solved (via solve).
| ||||||||||||||||

| ||||||||||||||||

Solve a goal by applying a function with some arguments filled in.
See refine for details.
| ||||||||||||||||

| ||||||||||||||||

Find a trivial solution to the goal by searching through the context for a premise which solves it immediately by refinement | ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

Eliminations | ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

Conversions | ||||||||||||||||

| ||||||||||||||||

Check that the goal is definitionally equal to the given term, and rewrite the goal accordingly. | ||||||||||||||||

| ||||||||||||||||

Normalise the goal | ||||||||||||||||

| ||||||||||||||||

Beta reduce in the goal | ||||||||||||||||

| ||||||||||||||||

Beta reduce the goal, unfolding the given function | ||||||||||||||||

Equality | ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

Computations | ||||||||||||||||

| ||||||||||||||||

Make a recursive call of a computation. The term must be an allowed recursive call, identified in the context by having a labelled type. | ||||||||||||||||

| ||||||||||||||||

Prepare to return a value in a computation | ||||||||||||||||

Staging | ||||||||||||||||

| ||||||||||||||||

Prepare to return a quoted value | ||||||||||||||||

Tactic combinators | ||||||||||||||||

| ||||||||||||||||

The Identity tactic, does nothing. | ||||||||||||||||

| ||||||||||||||||

Apply a sequence of tactics to the default goal. Read the type
as [Tactic] -> Tactic
| ||||||||||||||||

| ||||||||||||||||

Sequence two tactics; applies two tactics sequentially to the same goal | ||||||||||||||||

| ||||||||||||||||

Apply a tactic, then apply another to each subgoal generated. | ||||||||||||||||

| ||||||||||||||||

Apply a tactic, then apply the next tactic to the next default subgoal. | ||||||||||||||||

| ||||||||||||||||

Tries the left tactic, if that fails try the right one. Shorthand for
try x idTac y.
| ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

| ||||||||||||||||

The Tracing tactic; does nothing, but uses trace to dump the
current proof state
| ||||||||||||||||

Produced by Haddock version 2.4.2 |