sig
type split = {
lit_pos : Libzipperposition.Position.t;
term_pos : Libzipperposition.Position.t;
term : Literal.term;
}
val split : Literal.t -> Libzipperposition.Position.t -> Literal.Pos.split
val at : Literal.t -> Libzipperposition.Position.t -> Literal.term
val replace :
Literal.t ->
at:Libzipperposition.Position.t -> by:Literal.term -> Literal.t
val cut :
Literal.t ->
Libzipperposition.Position.t ->
Libzipperposition.Position.t * Libzipperposition.Position.t
val root_term : Literal.t -> Libzipperposition.Position.t -> Literal.term
val term_pos :
Literal.t -> Libzipperposition.Position.t -> Libzipperposition.Position.t
val is_max_term :
ord:Libzipperposition.Ordering.t ->
Literal.t -> Libzipperposition.Position.t -> bool
end