package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type

LogtkPositions in terms, clauses...

type t =
  1. | Stop
  2. | LogtkType of t
    (*

    Switch to type

    *)
  3. | Left of t
    (*

    Left term in curried application

    *)
  4. | Right of t
    (*

    Right term in curried application, and subterm of binder

    *)
  5. | Record_field of string * t
    (*

    Field of a record

    *)
  6. | Record_rest of t
    (*

    Extension part of the record

    *)
  7. | Head of t
    (*

    Head of uncurried term

    *)
  8. | 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