Function positive_increment

examples/06_effectful_verifier/python/main.py:47–51

(x: Annotated[int, Gt(0)])

def positive_increment(x: Annotated[int, Gt(0)]):
    y = x + 3
    assert_refined(y, Gt(3))  # x > 0 → x + 3 > 3   ✓
    z = x + 10
    assert_refined(z, Gt(10))  # x > 0 → x + 10 > 10  ✓


assert verify(positive_increment)