let add (x : {v:float|v>0} ) (y : {v:float|v>0} ) : { v:float | v >= x && v >= y} = let z = x +. y in z
let f6 (x : {v : float | v < 0 }) : {v : float | v > 0} = let y = x *. x in add y y
The previous code does not type checks, with the following error:
File "refinement_function_test.zls", line 59, characters 5-6:
add y y
^
Type error: this is a combinatorial expression and is expected to be static.
It seems that the first y argument is causing trouble because the following passes the type check
let f6 (x : {v : float | v < 0 }) : {v : float | v > 0} = let y = x *. x in add 1. y
let add (x : {v:float|v>0} ) (y : {v:float|v>0} ) : { v:float | v >= x && v >= y} = let z = x +. y in zlet f6 (x : {v : float | v < 0 }) : {v : float | v > 0} = let y = x *. x in add y yThe previous code does not type checks, with the following error:
It seems that the first y argument is causing trouble because the following passes the type check
let f6 (x : {v : float | v < 0 }) : {v : float | v > 0} = let y = x *. x in add 1. y