package logtk

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

Parameters

module A : AC_SPEC

Signature

val flatten : LogtkSymbol.t -> t list -> t list

flatten_ac f l flattens the list of terms l by deconstructing all its elements that have f as head symbol. For instance, if l=1+2; 3+(4+5) with f="+", this will return 1;2;3;4;5, perhaps in a different order

val normal_form : t -> t

normal form of the term modulo AC

val eq : t -> t -> bool

Check whether the two terms are AC-equal. Optional arguments specify which symbols are AC or commutative (by default by looking at attr_ac and attr_commut).

val symbols : t Sequence.t -> LogtkSymbol.Set.t

Set of symbols occurring in the terms, that are AC