Function _build_vc_expr

examples/06_effectful_verifier/python/refine.py:149–175

Convert an effectful VC Term to a ``Lean.Expr`` proposition. Builds ``∀ (x : Int) ..., preconds → body`` with correct de Bruijn indices at each binder depth.

(eb: ExprBuilder, vc_term, var_names, var_ops, precond_terms)

def _build_vc_expr(eb: ExprBuilder, vc_term, var_names, var_ops, precond_terms):
    """Convert an effectful VC Term to a ``Lean.Expr`` proposition.

    Builds ``∀ (x : Int) ..., preconds → body`` with correct de Bruijn
    indices at each binder depth.
    """
    n_vars = len(var_names)
    n_preconds = len(precond_terms)
    total = n_vars + n_preconds

    # Evaluate the body at the innermost depth (all binders above).
    with handler(_make_expr_handler(eb, var_names, var_ops, total)):
        body_expr = evaluate(vc_term)

    # Wrap preconditions from innermost outward.
    result = body_expr
    for j in reversed(range(n_preconds)):
        depth = n_vars + j
        with handler(_make_expr_handler(eb, var_names, var_ops, depth)):
            prec_expr = evaluate(precond_terms[j])
        result = eb.mk_forall("_", prec_expr, result)

    # Wrap ∀ variable binders.
    for i in reversed(range(n_vars)):
        result = eb.mk_forall(var_names[i], eb.INT, result)

    return result


# ---------------------------------------------------------------------------