Open jlvargasme opened 2 years ago
let add (x : {v : float | v < 0 }) (y : {v : float | v < 0 }) : { v : float | v >= 0} = x x + yy
Once the function is called, for example, let s = add 1 (-.3)
We want to verify that "not ( (x = 1 and y = -3) -> (x < 0 and y < 0))"
In this example, the check should fail since 1 !< 0.
let add (x : {v : float | v < 0 }) (y : {v : float | v < 0 }) : { v : float | v >= 0} = x x + yy
Once the function is called, for example, let s = add 1 (-.3)
We want to verify that "not ( (x = 1 and y = -3) -> (x < 0 and y < 0))"
In this example, the check should fail since 1 !< 0.