proof.term
Class Sigma

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

All Implemented Interfaces:

java.io.Serializable, Term

public class Sigma

extends java.lang.Object

implements Term

A sigma type. Exactly as in any other Calculus of Constructions implementation, except that we use field selectors instead of fst and snd.

See Also:

Serialized Form

Field Summary

Term	A The types of the components.
Term	B The types of the components.
Var	x The bound variable.

Constructor Summary

Sigma(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 types of the components. x is considered to be of type A, and B (the type of b) can depend on x.

B

public 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.

Constructor Detail

Sigma

public Sigma(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.