sig
  type specific_equality = {
    for_tau : Wp.Lang.F.tau -> bool;
    mk_new_eq : Wp.Lang.F.binop;
  }
  val rebuild :
    ?cache:Wp.Lang.F.term Wp.Lang.F.Tmap.t ->
    Wp.Lang.F.term -> Wp.Lang.F.term * Wp.Lang.F.term Wp.Lang.F.Tmap.t
  val set_builtin :
    Wp.Lang.Fun.t -> (Wp.Lang.F.term list -> Wp.Lang.F.term) -> unit
  val set_builtin' :
    Wp.Lang.Fun.t ->
    (Wp.Lang.F.term list -> Wp.Lang.F.tau option -> Wp.Lang.F.term) -> unit
  val set_builtin_eq :
    Wp.Lang.Fun.t ->
    (Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term) -> unit
  val set_builtin_leq :
    Wp.Lang.Fun.t ->
    (Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term) -> unit
  val in_state : ('-> 'b) -> '-> 'b
end