module Quantif:sig
..end
Convert quantifiers.
val quantif_to_exp : Cil_types.kernel_function ->
Env.t -> Cil_types.predicate -> Cil_types.exp * Env.t
The given predicate must be a quantification.
val predicate_to_exp_ref : (adata:Assert.t ->
Cil_types.kernel_function ->
Env.t -> Cil_types.predicate -> Cil_types.exp * Assert.t * Env.t)
Stdlib.ref
Forward reference for Translate_predicates.to_exp
.