proof.type
Class UnivBinding

java.lang.Object
  |
  +--proof.term.Var
        |
        +--proof.type.Context
              |
              +--proof.type.UnivBinding

All Implemented Interfaces:

java.io.Serializable, Term

public class UnivBinding

extends Context

Binds a variable in some Context.

See Also:

Serialized Form

Fields inherited from class proof.type.Context

level, parent

Fields inherited from class proof.term.Var

name

Constructor Summary

protected

UnivBinding(java.lang.String name, Context parent, Term type) Constructor for "making assumptions." (Note that it's protected, since this amounts to "adding an axiom.")

Method Summary

java.lang.String	contextToString() Format this as a String.
Term	getType() Read-only access to the type of this binding.
int	numberOfHoles() Counts the number of ExistBindings ("holes") in this Context.
protected Context	substituteIntoContext(Var x, Context c, Term s) Substitute into this Context entry.
boolean	wellTypedUsingConstraints() This is well-formed using the constraints if it's a valid type in its parent Context.

Methods inherited from class proof.type.Context

headReduceContextOnce, wellFormedUsingConstraints

Methods inherited from class proof.term.Var

alphaEquals, headReduceOnce, substitute, toString

Methods inherited from class java.lang.Object

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

Constructor Detail

UnivBinding

protected UnivBinding(java.lang.String name,
                      Context parent,
                      Term type)

Constructor for "making assumptions." (Note that it's protected, since this amounts to "adding an axiom.")

Parameters:

name - the name of the variable being bound

parent - the Context being extended

type - the type of the variable being assumed

Method Detail

getType

public Term getType()

Read-only access to the type of this binding.

substituteIntoContext

protected Context substituteIntoContext(Var x,
                                        Context c,
                                        Term s)

Substitute into this Context entry. We assume that no-one will try to substitute into a UnivBinding.

Overrides:

substituteIntoContext in class Context

Following copied from class: proof.type.Context

Parameters:

x - the variable to substitute in for

c - the Context to add to the left of that variable (it should extend the context that's to the left of x)

s - the Term to substitute in

wellTypedUsingConstraints

public boolean wellTypedUsingConstraints()

This is well-formed using the constraints if it's a valid type in its parent Context.

numberOfHoles

public int numberOfHoles()

Counts the number of ExistBindings ("holes") in this Context. If this is zero, then there are no "holes" left, and this is a "success context."

Overrides:

numberOfHoles in class Context

contextToString

public java.lang.String contextToString()

Format this as a String.

Overrides:

contextToString in class Context