|
| |
|
| java.lang.Object
 de.uka.ilkd.key.logic.PosInTerm
| PosInTerm | | public class PosInTerm (Code) | | |
| TOP_LEVEL | | final public static PosInTerm TOP_LEVEL(Code) | | top level term position
|
| depth | | public int depth()(Code) | | size of the position list
|
| down | | public PosInTerm down(int n)(Code) | | descending downwards choosing the n'th subterm, subformula
Parameters:
n - int describs the chosen subterm Position like old Position but with a deepersubterm. |
| equals | | public boolean equals(Object obj)(Code) | | compares this PosInTerm with another PosInTerm
and returns true if both describe the same position
|
| getIndex | | public int getIndex()(Code) | | the number/index of the deepest subterm that thisPosInTerm points to. If the position is top-level,the result will be -1 |
| hashCode | | public int hashCode()(Code) | | |
| iterator | | public IntIterator iterator()(Code) | | returns an iterator defining the position in a term according to
subterm relation. A PosInTerm defining the xn'th subterm of the
x(n-1)'th subterm of ... of the x1'th subterm of a term returns an
iterator subsequently resulting in the list x1...xn.
an iterator over the list defining the position in a term. |
| reverseIterator | | public IntIterator reverseIterator()(Code) | | get subterm/-formula information. A PosInTerm defining the xn'th
subterm of the x(n-1)'th subterm of ... of the x1'th subterm of a
term returns an iterator subsequently resulting in the list xn...x1.
IteratorOfInteger that iterates through the subtermsof a sequent in the reverse order as the PosInTerm has been defined. |
|
|
|