Full description of a position in a literal. It contains:
lit_pos: the literal-prefix of the positionterm_pos: the suffix that describes a subterm positionterm: the term root, just under the literal itself. given this, applying T.Pos.at to the subterm position and the root term we obtain the sub-term itself.val split : t -> Position.t -> splitInvalid_argument if the position is incorrect
val at : t -> Position.t -> termSubterm at given position, or
Invalid_argument if the position is invalid
val replace : t -> at:Position.t -> by:term -> tReplace subterm, or
Invalid_argument if the position is invalid
val cut : t -> Position.t -> Position.t * Position.tcut the subterm position off. For instance a position "left.1.2.stop" in an equation "l=r" will yield "left.stop", "1.2.stop".
it always holds that let a,b = cut p in Position.append a b = p
val root_term : t -> Position.t -> termObtain the term at the given position, at the root of the literal. It should hold that root_term lit p = [at lit (fst (cut p))].
val term_pos : t -> Position.t -> Position.tterm_pos lit p = snd (cut lit p), the subterm position.
val is_max_term : ord:Ordering.t -> t -> Position.t -> boolIs the term at the given position, maximal in the literal w.r.t this ordering? In other words, if the term is replaced by a smaller term, can the whole literal becomes smaller?