Serialized Form

Class proof.term.Abstr implements Serializable

Serialized Fields

x

Var x

The bound variable. When the Abstraction is copied, or substituted into, this is copied as well.

type

Term type

The type of the variable.

s

Term s

The body of the abstraction.

Class proof.term.Appl implements Serializable

Serialized Fields

rator

Term rator

The term being applied.

rand

Term rand

The argument.

Class proof.type.Context implements Serializable

Serialized Fields

parent

Context parent

The Context that this extends.

level

int level

The level of this term in the context. This is used when we're comparing terms for beta-convertability. We can possibly just reduce the head of the term with the higher level. Now that I see how useful the depths are for lazily checking alpha-convertability, I start to wonder about using the de Bruijn nameless representation after all...

Class proof.term.EmptyRecord implements Serializable

Class proof.term.EmptyRecordType implements Serializable

Class proof.type.ExistBinding implements Serializable

Serialized Fields

type

Term type

The type of this variable.

localContext

Context localContext

The "local context", which contains UnivBindings variables which may be used to inhabit this term. When this ExistBinding is substituted into, this is "inherited" from the parent Context. FIXME: there are a bunch of ugly hacks associated with this

Class proof.term.Field implements Serializable

Serialized Fields

record

Term record

The term we're taking a field of.

label

java.lang.String label

The label of the field.

Class proof.term.Pair implements Serializable

Serialized Fields

x

Var x

The bound variable.

a

Term a

The two components of the pair. x is considered to have the value a, and b can contain the variable x.

b

Term b

The two components of the pair. x is considered to have the value a, and b can contain the variable x.

Class proof.term.Pi implements Serializable

Serialized Fields

x

Var x

The bound variable. When the pi abstraction is copied, or substituted into, this is copied as well.

type

Term type

The type of the variable.

s

Term s

The body of the abstraction.

Class proof.prove.ProverApplet implements Serializable

Serialized Fields

exprText

java.awt.TextArea exprText

TextArea for displaying a Term (if it's found.)

typeText

java.awt.TextArea typeText

TextArea for entering the type to try to inhabit.

depthField

java.awt.TextField depthField

Field indicating how deeply to search for a proof.

maxHolesField

java.awt.TextField maxHolesField

Field indicating how many holes (existential variables) to allow in a proof.

Class proof.term.Sigma implements Serializable

Serialized Fields

x

Var x

The bound variable.

A

Term A

The types of the components. x is considered to be of type A, and B (the type of b) can depend on x.

B

Term B

The types of the components. x is considered to be of type A, and B (the type of b) can depend on x.

Class proof.term.Sort implements Serializable

Serialized Fields

sort

int sort

Which sort this is.

Class proof.type.TypecheckerTestApplet implements Serializable

Serialized Fields

exprText

java.awt.TextArea exprText

TextArea for inputting an environment to parse and typecheck.

typeText

java.awt.TextArea typeText

TextArea for displaying the result of typechecking that.

Class proof.type.TypecheckFailedException implements Serializable

Class proof.type.UnivBinding implements Serializable

Serialized Fields

type

Term type

The type of this variable.

Class proof.term.Var implements Serializable

Serialized Fields

name

java.lang.String name

The name of the variable. This will basically be for debugging purposes.