Module Logtk.Position (.ml)

module Position: LogtkPosition

type t = 
| Stop
| LogtkType 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
*)
| Record_field of string * t (*
Field of a record
*)
| Record_rest of t (*
Extension part of the record
*)
| Head of t (*
Head of uncurried term
*)
| Arg of int * t (*
argument term in uncurried term, or in multiset
*)
A position is a path in a tree
type position = t 
val stop : t
val left : t -> t
val right : t -> t
val type_ : t -> t
val record_field : string -> t -> t
val record_rest : t -> t
val head : 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 compare : t -> t -> int
val eq : t -> t -> bool
val hash : t -> int
val pp : Buffer.t -> t -> unit
val fmt : Format.formatter -> t -> unit
val to_string : t -> string

LogtkPosition builder


module Build: sig .. end