logtk

Core types and algorithms for logic
IN THIS PACKAGE
Module Logtk . Literals . Pos
val at : t -> Position.t -> term

Return the subterm at the given position, or

  • raises Invalid_argument

    if the position is not valid

val lit_at : t -> Position.t -> Literal.t * 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 : t -> at:Position.t -> by: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 : Position.t -> int

Index in the literal array

  • raises Invalid_argument

    if the position is incorrect

val tail : Position.t -> Position.t

sub-position

  • raises Invalid_argument

    if the position is incorrect

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

Index + literal position