Module Wp.Lang.For_export

module For_export: sig .. end

For why3_api but circular dependency


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 : ('a -> 'b) -> 'a -> 'b