Module Logtk.Position

Positions in terms, clauses...

type t =
| Stop
| Type of t

Switch to type

| Left of t

Left term in curried application

| Right of t

Right term in curried application, and subterm of binder

| Head of t

Head of uncurried term

| Arg of int * t

argument term in uncurried term, or in multiset

| Body of t

Body of binder or horn clause

A position is a path in a tree

type position = t
val stop : t
val type_ : t -> t
val left : t -> t
val right : t -> t
val head : t -> t
val body : t -> t
val arg : int -> t -> t
val opp : t -> t

Opposite position, when it makes sense (left/right)

val rev : t -> t

Reverse the position

val append : t -> t -> t

Append two positions

val is_prefix : t -> t -> bool

is_prefix a b is true iff a is a prefix of b

val is_strict_prefix : t -> t -> bool

is_prefix a b is true iff a is a prefix of b and a != b

val compare : t -> t -> int
val equal : t -> t -> bool
val hash : t -> int
val num_of_funs : t -> int
val until_first_fun : t -> t
include Interfaces.PRINT with type t := t
type t
val pp : t CCFormat.printer
val to_string : t -> string
module Map : sig ... end

Position builder

module Build : sig ... end

Pairing of value with Pos

module With : sig ... end