Frama-C:
Plug-ins:
Libraries:

Frama-C API - For_export

For why3_api but circular dependency

type specific_equality = {
  1. for_tau : F.tau -> bool;
  2. 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