find_term id s returns the term together with its type, as declared or defined in the signature s, corresponding to the symbol id in s if it exists. Raise Not_found otherwise
is_constant id s returns (true,Some (b,pred)) together with its syntactic behaviour b and its precedence pred if id is the name of a constant in s and false,None oterwise
precedence id s returns a Some f where f is float indicating the precedence of the infix operator id. It returns None if id is not an infix operator.
val new_precedence : ?before:string ->string ->t-> float * t
new_precedence ?before id s returns a pair consisting of a new precedence value associated to id, and the new signature taking this new value into account. If the optional string argument before is not provided, then id is given the highest precedence so far. Otherwise, it is given the precedence just below before.
unfold_type_definition id t returns the actual type for the type defined by id as the identifier of a type definition in the signature t. Fails with "Bug" if id does not correspond to a type definition
unfold_term_definition id t returns the actual term for the term defined by id as the identifier of a term definition in the signature t. Fails with "Bug" if id does not correspond to a term definition
fold f a sg returns f e_n (f e_n-1 ( ... ( f e_1 a) ... )) where the e_i are the entries of the signature sg. It is ensured that the e_i are provided in the same order as they have been inserted.