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 size : t -> int
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 Logtk.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