Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved
PREV CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD

## escjava.prover
Class SPair

    java.lang.Object
      escjava.prover.SExp
          escjava.prover.SList
              escjava.prover.SPair

class SPair
extends SList

A `SPair` is a pair of a `SExp` and a `SList`; together with the `SNil` class, it is used to implement lists of `SExp`s.

Considered as `SList`s, `SPair`s always represent non-empty lists.

Field Summary
`SExp` | `head` The head of our list; this field should not be modified by clients and should be non-null.
`SList` | `tail` The tail of our list; this field should not be modified by clients and should be non-null.

Constructor Summary
`SPair(SExp head, SList tail)` Return a new list with given head and tail.

Method Summary
`boolean` | `equals(java.lang.Object o)` Return true if the heads are equal and the tails are equal.
`(package private) SPair` | `getPair()` If we represent a non-empty list, return it as a `SPair`; otherwise, throw `SExpTypeError`.
`boolean` | `isEmpty()` Are we an empty list?
`int` | `length()` Return our length

Methods inherited from class escjava.prover.SList
`addEnd, addFront, append, at, fromArray, getList, isList, main, make, make, make, make, make, make, make, make, make, prettyPrint, print, reverseD, setAt`

Methods inherited from class escjava.prover.SExp
`display, fancyMake, getAtom, getInteger, isAtom, isInteger, make, print, toString`

Methods inherited from class java.lang.Object
`clone, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait`

Field Detail

### head

    public SExp head

  The head of our list; this field should not be modified by clients and should be non-null.

### tail

    public SList tail

  The tail of our list; this field should not be modified by clients and should be non-null.

Constructor Detail

### SPair

    public SPair(SExp head,
                 SList tail)

  Return a new list with given head and tail.

  Both must be non-null.

Method Detail

### isEmpty

    public boolean isEmpty()

  Are we an empty list?

  Specified by:
    `isEmpty` in class `SList`
  Returns:
    a flag indicating if we are we an empty list.

### getPair

    SPair getPair()

  If we represent a non-empty list, return it as a `SPair`; otherwise, throw `SExpTypeError`.

  Overrides:
    `getPair` in class `SList`

### length

    public int length()

  Return our length

  Specified by:
    `length` in class `SList`
  Returns:
    our length.

### equals

    public boolean equals(java.lang.Object o)

  Return true if the heads are equal and the tails are equal.

Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved
PREV CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD

The ESC/Java2 Project Homepage