Module Algebra.Presentation.M

module M: Monoid.Free(X)

type t = X.t array

type word = t

val mul : t -> t -> t

val one : t

val inj : X.t -> t

val length : t -> int

val sub : t -> int -> int -> t

val eq : t -> t -> bool

val compare : t -> t -> int

val peq : t -> int -> t -> int -> int -> bool

Partial equality (equality on subwords).

val to_string : t -> string

val included : t -> t -> bool

val unifier : ?i:int -> t -> t -> int

The leftmost unifier where u is on the left and v on the right

val ordered_unifiers : t -> t -> int list

All unifiers with first on the left.

val ordered_unifiers_bicontext : t ->
       t ->
       ((t * t) * (t * t)) list

val unifiers_bicontext : t ->
       t ->
       ((t * t) * (t * t)) list

All unifiers, with contexts on the left and on the right.

module Order: sig .. end

module Anick: sig .. end

Anick chains.