module Symbol:Symbols.sig
..end
type
t
val equal : t -> t -> bool
val hash : t -> int
val compare : t -> t -> int
val name_declared : string -> bool
name_declared n
is true when a symbol has been declared with name n.val declare : string -> int -> t
declare n a
declares a new symbol with the name n
and arity a
which is interpreted by some theory.
a >= 0
not (name_declared n)
val declare_uninterpreted : string -> int -> t
declare
, but for an uninterpreted symbolval find : string -> t
find n
is the symbol declared with name n
.Not_found
when not (name_declared n)
val arity : t -> int
arity s
is the arity declared for s
.val interpreted : t -> bool
val string_of_symbol : t -> string
val pp_print : Format.formatter -> t -> unit
module Primitive:sig
..end