Module Quantif

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.

Forward references


val predicate_to_exp_ref : (Cil_types.kernel_function ->
Env.t -> Cil_types.predicate -> Cil_types.exp * Env.t)
Pervasives.ref
val term_to_exp_ref : (Cil_types.kernel_function ->
Env.t -> Cil_types.term -> Cil_types.exp * Env.t)
Pervasives.ref