proof.term
Class Sort

java.lang.Object
  |
  +--proof.term.Sort

All Implemented Interfaces:

java.io.Serializable, Term

public class Sort

extends java.lang.Object

implements Term

A sort.

See Also:

Serialized Form

Field Summary

static int	BOX
static int	EXTERN
int	sort Which sort this is.
static int	STAR Constants for the two sorts, plus the one used in proof search.

Constructor Summary

Sort(int sort)
Constructor which expects Sort.STAR or Sort.BOX .

Sort(java.lang.String sort)
Constructor.

Method Summary

boolean	alphaEquals(Term t) Compares this term to another term, up to variable renaming.
Term	headReduceOnce() ...
Term	substitute(Var y, Term s) Substituting into this does nothing...
java.lang.String	toString() Convert this term to a String.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

STAR

public static final int STAR

Constants for the two sorts, plus the one used in proof search.

BOX

public static final int BOX

EXTERN

public static final int EXTERN

sort

public int sort

Which sort this is.

Constructor Detail

Sort

public Sort(java.lang.String sort)

Constructor.

Sort

public Sort(int sort)

Constructor which expects Sort.STAR or Sort.BOX .

Method Detail

substitute

public Term substitute(Var y,
                       Term s)

Substituting into this does nothing...

Specified by:

substitute in interface Term

Following copied from interface: proof.term.Term

Parameters:

y - the Var to substitute in for

t - the term to substitute in.

Returns:

the result of substituting

headReduceOnce

public Term headReduceOnce()

... and reducing is easy.

Specified by:

headReduceOnce in interface Term

Following copied from interface: proof.term.Term

Returns:

this term, reduced once

alphaEquals

public boolean alphaEquals(Term t)

Description copied from interface: Term

Compares this term to another term, up to variable renaming.

Specified by:

alphaEquals in interface Term

Following copied from interface: proof.term.Term

Parameters:

t - the term to compare this to

Returns:

true iff this and t are equal (ignoring the names of variables)

toString

public java.lang.String toString()

Convert this term to a String.

Specified by:

toString in interface Term

Overrides:

toString in class java.lang.Object