Module `Builtin.Fun`

Builtin functions

type t = private { id : Uid.t; name : attr_name; }

val id : t -> Uid.t
val attr_name : t -> attr_name: unique name in [\@\@z3 name]

val mem : attr_name -> bool

val find : attr_name -> t

raises Not_found: if this builtin function was not registered

val register : ?⁠as_tip:string -> attr_name -> Uid.t -> t: memorize that this Uid corresponds to the given builtin fun

val get_and : unit -> t
val get_or : unit -> t
val get_not : unit -> t
val get_implies : unit -> t
val get_eq : unit -> t
val get_neq : unit -> t
val get_iff : unit -> t
val get_i_add : unit -> t
val get_i_sub : unit -> t
val get_float_eq : unit -> t
val get_float_neq : unit -> t
val is_list_hd : Uid.t -> bool
val is_list_tl : Uid.t -> bool
val is_eq : Uid.t -> bool
val is_neq : Uid.t -> bool
val is_not : Uid.t -> bool
val is_implies : Uid.t -> bool
val is_and : Uid.t -> bool
val is_or : Uid.t -> bool
val is_iff : Uid.t -> bool
val is_i_add : Uid.t -> bool
val is_i_sub : Uid.t -> bool
val is_i_mul : Uid.t -> bool
val is_i_div : Uid.t -> bool
val is_leq : Uid.t -> bool
val is_lt : Uid.t -> bool
val is_geq : Uid.t -> bool
val is_gt : Uid.t -> bool