#### logtk 2.1 2.0 1.6 1.5.1 0.8.1

Core types and algorithms for logic
IN THIS PACKAGE
Module .

## Positions in terms, clauses...

Positions are used to indicate a given occurrence of an object in a tree-like structure.

Typically, we use positions to refer to a particular occurrence of a term in another (bigger) term, or in a literal, or in a clause.

A pair of `{term,clause,literal}` + position represents a context, that is, a `{term,clause,literal}` with a hole at the given position, where we can put a different term.

`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 Interfaces.PRINT with type t := 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

Positions act a bit like lenses, in the sense that they compose nicely and designat paths in objects

`module With : sig ... end`