module For_export: sig
.. end
For why3_api but circular dependency
type
specific_equality = {
}
val rebuild : ?cache:Lang.F.term Lang.F.Tmap.t ->
Lang.F.term -> Lang.F.term * Lang.F.term Lang.F.Tmap.t
val set_builtin : Lang.Fun.t -> (Lang.F.term list -> Lang.F.term) -> unit
val set_builtin' : Lang.Fun.t -> (Lang.F.term list -> Lang.F.tau option -> Lang.F.term) -> unit
val set_builtin_eq : Lang.Fun.t -> (Lang.F.term -> Lang.F.term -> Lang.F.term) -> unit
val set_builtin_leq : Lang.Fun.t -> (Lang.F.term -> Lang.F.term -> Lang.F.term) -> unit
val in_state : ('a -> 'b) -> 'a -> 'b