module Pos: sig .. end
val at : Literals.t -> Libzipperposition.Position.t -> Literals.term
Return the subterm at the given position, or
Raises Invalid_argument if the position is not valid
val lit_at : Literals.t ->
Libzipperposition.Position.t -> Literal.t * Libzipperposition.Position.t
Lookup which literal the position is about, return it
and the rest of the position.
Raises Invalid_argument if the position is not valid
val replace : Literals.t -> at:Libzipperposition.Position.t -> by:Literals.term -> unit
In-place modification of the array, in which the subterm at given
position is replaced by the by term.
Raises Invalid_argument if the position is not valid
val idx : Libzipperposition.Position.t -> int
Index in the literal array
Raises Invalid_argument if the position is incorrect
val tail : Libzipperposition.Position.t -> Libzipperposition.Position.t
sub-position
Raises Invalid_argument if the position is incorrect
val cut : Libzipperposition.Position.t -> int * Libzipperposition.Position.t
Index + literal position