proof.term
Class Pi

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

All Implemented Interfaces:

java.io.Serializable, Term

public class Pi

extends java.lang.Object

implements Term

A Pi abstraction.

See Also:

Serialized Form

Field Summary

Term	s The body of the abstraction.
Term	type The type of the variable.
Var	x The bound variable.

Constructor Summary

Pi(Var x, Term type, Term s)
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 term's body.
Term	substitute(Var y, Term t) Substitute into this term.
java.lang.String	toString() Convert this to a String.

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. When the pi abstraction is copied, or substituted into, this is copied as well.

type

public Term type

The type of the variable.

s

public Term s

The body of the abstraction.

Constructor Detail

Pi

public Pi(Var x,
          Term type,
          Term s)

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 term's body. Or reduce inside the type.

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