Function assert_refined

examples/06_effectful_verifier/python/refine.py:57–63

Declare that *value* satisfies *refinement*. During symbolic execution, the handler intercepts this and collects the verification condition as a ``Term[bool]``.

(value: int, refinement)

@defop
def assert_refined(value: int, refinement) -> None:
    """Declare that *value* satisfies *refinement*.

    During symbolic execution, the handler intercepts this and collects the
    verification condition as a ``Term[bool]``.
    """
    pass  # no-op in concrete mode


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