The proof language for type conversions |

### Internal representation of proofs

Internally, a `Proof`
instance is encoded by an expression tree of type `GEN` (which equals `Generic`), each subtree being either of
type `Literal` or `Compound`. The private
conversion routines between the types `Proof`
and `GEN` are `postfix .v` and `proof`.
The public routines for the syntactic manipulation of proofs are

`proof$literal: Literal ->
Proof`

`literal?: Proof ->
Boolean`

`convert: Proof ->
Literal`

Creation of a leaf, testing whether a proof is a leaf and converting
a leaf to a literal.

`postfix (): (Proof, Tuple Proof) ->
Proof`

`compound?: Proof ->
Boolean`

`prefix #: Proof ->
Int`

`postfix []: (Proof, Int) ->
Proof`

Creation of a compound tree, testing whether an proof is a compound
tree, obtaining the arity of a compound tree and accessing a child
of a compound tree.

### Internal representation of problems

### Syntactic utility routines

`postfix .components: Proof ->
Proofs`

`postfix .args: Proof ->
Proofs`

`postfix .initial: Proof ->
Proofs`

`postfix .last: Proof ->
Proof`

Commodity accessors for the determination of all components of a
compound tree (`postfix
.components`), of all arguments of a primitive or
function call (`postfix
.args`), of all but its last arguments (`postfix .initial`), and its last
argument (`postfix
.args`).

`subst (pr: Proof, what: Proof, by:
Proof): Proof`

`subst (pr: Proof, t: TABLE):
Proof`

Syntactic substitution of `what`
by `by` in `pr`, or of each variable `var` in the table `t` by `var[t]`.

### General proof logic

`$rule (ax: Proof, val: Proof):
Proof`

Construct for basic axioms: the axiom `ax`
corresponds to a type convertability assertion, such as `$converts (F, T)`, and the value `val` to the algorithm
which implements the conversion. Rules are usually templated using
the `$forall` construct

Mark a part of a proof as being not yet solved.

`$forall (ql: PRGS, pr: Proof):
Proof`

`$exists (ql: PRGS, pr: Proof):
Proof`

Universal and existential quantification.

`$implies (p1: Proof, p2: Proof):
Proof`

`$and (p1: Proof, p2: Proof):
Proof`

`$or (p1: Proof, p2: Proof):
Proof`

Basic logical connectors.

### Type conversion logic

`converts (t1: TYP, t2: TYP):
Proof`

The assertion that the type `t1`
can be converted into the type `t2`.

© 2010 Joris van der Hoeven

Permission is granted to copy, distribute and/or modify this document
under the terms of the

GNU General Public License. If you
don't have this file, write to the Free Software Foundation, Inc., 59
Temple Place - Suite 330, Boston, MA 02111-1307, USA.