Module Lang.For_export

For why3_api but circular dependency

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