#### logtk

Core types and algorithms for logic
IN THIS PACKAGE
Module . .

### Positions

`type split = {`
 `lit_pos : Position.t;` `term_pos : Position.t;` `term : term;`
`}`

Full description of a position in a literal. It contains:

• `lit_pos`: the literal-prefix of the position
• `term_pos`: the suffix that describes a subterm position
• `term`: 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 -> split`
• raises Invalid_argument

if the position is incorrect

`val at : t -> Position.t -> term`

Subterm at given position, or

• raises Invalid_argument

if the position is invalid

`val replace : t -> at:Position.t -> by:term -> t`

Replace subterm, or

• raises Invalid_argument

if the position is invalid

`val cut : t -> Position.t -> Position.t * Position.t`

cut 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 -> term`

Obtain 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.t`

`term_pos lit p = snd (cut lit p)`, the subterm position.

`val is_max_term : ord:Ordering.t -> t -> Position.t -> bool`

Is 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?