[1.2]
for instance stands for the third subterm
(2, starting at 0) in the second subterm (1) the term. []
stands for term itself.
SubtermSelectors can be wrapped in a TermSelector which selects a term from
a sequent. S.3.[1.2]
would select the above subterm from
the fourth (3) term of the succedent (S) of the sequent.
Term | TermSelector | Linear index |
---|---|---|
f(g(x,y), z) | [] | 0 |
g(x,y) | [0] | 1 |
x | [0.0] | 2 |
y | [0.1] | 3 |
z | [1] | 4 |