logtk

Core types and algorithms for logic
IN THIS PACKAGE
Module Logtk . Monome . Rat
type t = Q.t monome
val const : Q.t -> t

Empty monomial, from constant (decides type)

val singleton : Q.t -> term -> t

One term.

val of_list : Q.t -> (Q.t * term) list -> t
val divide : t -> Q.t -> t

Divide by non-zero constant

val of_term : term -> t option
val of_term_exn : term -> t

try to get a monome from a term.

  • raises NotLinear

    if the term is not a proper monome.

val to_term : t -> term

convert back to a term

val to_multiset : t -> Multisets.MT.t

Multiset of terms