module Rac:sig
..end
typeoracle_quant_var =
Pinterp_core.env -> Term.vsymbol -> Pinterp_core.Value.value option
An oracle to get all-quantified variables during RAC. Used to progress
when the transformation "compute_in_goal"
blocks on a quantifier.
val oracle_quant_var_dummy : oracle_quant_var
Always returns in None
.
val oracle_quant_var : ?bind_univ_quant_vars:bool ->
?bind_univ_quant_vars_default:bool ->
Pinterp_core.oracle -> oracle_quant_var
Derive an oracle for quantified variables from a normal oracle.
module Why:sig
..end
RAC implementation using a Why3 transformation and prover