Function _verify_expr

examples/06_effectful_verifier/python/refine.py:242–255

Create a goal from a ``Lean.Expr`` and close it. Uses ``simp [Int.ofNat]`` to normalise the fully-elaborated Int literals before ``omega`` decides the linear arithmetic.

(lib, kernel, lean_expr)

def _verify_expr(lib, kernel, lean_expr) -> bool:
    """Create a goal from a ``Lean.Expr`` and close it.

    Uses ``simp [Int.ofNat]`` to normalise the fully-elaborated Int
    literals before ``omega`` decides the linear arithmetic.
    """
    try:
        gs_handle = lib.effectful_goal_from_expr(lean_expr)
        gs = GoalState(kernel, gs_handle)
        result = gs.try_tactic("intros; simp [Int.ofNat] at *; omega")
        return result.ok and result.state is not None and result.state.is_solved()
    except Exception as exc:
        print(f"    [verify error: {exc}]")
        return False