Closed jlvargasme closed 2 years ago
let x_abs x : {v : float | v >= 0} = if x < 0 then -x else x
For this example we want to check both options of the if statement and prove that either branch makes the return condition of the function true
VC: "not ( ((x < 0) -> (-x >= 0)) and ( not (x < 0) -> (x >= 0)) )"
Implemented in #61
jchen-cs
commented
2 years ago jchen-cs
commented
2 years ago
let x_abs x : {v : float | v >= 0} = if x < 0 then -x else x
For this example we want to check both options of the if statement and prove that either branch makes the return condition of the function true
VC: "not ( ((x < 0) -> (-x >= 0)) and ( not (x < 0) -> (x >= 0)) )"