module SMap : module type of LogtkSymbol.Maptype t = private LogtkType.t SMap.tA signature maps symbols to types
val empty : tEmpty signature
val is_empty : t -> boolval singleton : LogtkSymbol.t -> LogtkType.t -> tval mem : t -> LogtkSymbol.t -> boolIs the symbol declared?
val declare : t -> LogtkSymbol.t -> LogtkType.t -> tDeclare the symbol, or
LogtkType.Error if the symbol is already defined with a different type
Invalid_argument if the type has free variables
val find : t -> LogtkSymbol.t -> LogtkType.t optionLookup the type of a symbol
val find_exn : t -> LogtkSymbol.t -> LogtkType.tLookup the type of a symbol
Not_found if the symbol is not in the signature
val arity : t -> LogtkSymbol.t -> int * intArity of the given symbol, or failure. see LogtkType.arity for more details about the returned value.
Not_found if the symbol is not in the signature
val cardinal : t -> intNumber of symbols
val is_ground : t -> boolOnly ground types?
Merge two signatures together.
LogtkType.Error if they share some symbols with distinct types
val filter : t -> (LogtkSymbol.t -> LogtkType.t -> bool) -> tOnly keep part of the signature
diff s1 s2 contains the symbols of s1 that do not appear in s2. Useful to remove base symbols.
val well_founded : t -> boolAre there some symbols of arity 0 in the signature?
true iff the Herbrand term universe of this signature is non empty
module Seq : sig ... endval to_set : t -> LogtkSymbol.Set.tSet of symbols of the signature
val to_list : t -> (LogtkSymbol.t * LogtkType.t) listval of_list : (LogtkSymbol.t * LogtkType.t) list -> tval iter : t -> (LogtkSymbol.t -> LogtkType.t -> unit) -> unitval fold : t -> 'a -> ('a -> LogtkSymbol.t -> LogtkType.t -> 'a) -> 'amodule TPTP : sig ... end