proof.term
Class Pair

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

All Implemented Interfaces:

java.io.Serializable, Term

public class Pair

extends java.lang.Object

implements Term

A (dependent) pair of terms, in which the second component may depend on the first component. This is just like conventional sigma-types, except that we use field selectors instead of fst and snd.

See Also:

Serialized Form

Field Summary

Term	a The two components of the pair.
Term	b The two components of the pair.
Var	x The bound variable.

Constructor Summary

Pair(Var x, Term a, Term b)
Constructor.

Method Summary

boolean	alphaEquals(Term t) Compares this term to another term, up to variable renaming.
Term	headReduceOnce() To reduce this, reduce inside the two components.
Term	substitute(Var y, Term t) Substitute into this term.
java.lang.String	toString() Convert this to a String.
java.lang.String	toStringWithoutBraces() Same as above, but leaves off the braces

Methods inherited from class java.lang.Object

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

Field Detail

x

public Var x

The bound variable.

a

public Term a

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

b

public Term b

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

Constructor Detail

Pair

public Pair(Var x,
            Term a,
            Term b)

Constructor.

Method Detail

substitute

public Term substitute(Var y,
                       Term t)

Substitute into this term.

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()

To reduce this, reduce inside the two components.

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 to a String.

Specified by:

toString in interface Term

Overrides:

toString in class java.lang.Object

toStringWithoutBraces

public java.lang.String toStringWithoutBraces()

Same as above, but leaves off the braces