The following expression does not pass the compiler check
let add (x : {v:int |v>0} ) (y : {v:int|v>0} ) : { v:int | v >= x && v >= y} = let z = x + y in z
However, if int is replaced with a float it works:
let add (x : {v:float|v>0} ) (y : {v:float|v>0} ) : { v:float | v >= x && v >= y} = let z = x +. y in z
The issue is that MARVeLus has no type inference mechanism to determine the type of z, which then default to float. When assigning "z = x + y" in Z3, it implicitly creates a new float x and a new float y, which then breaks the system.
The following expression does not pass the compiler check
let add (x : {v:int |v>0} ) (y : {v:int|v>0} ) : { v:int | v >= x && v >= y} = let z = x + y in zHowever, if int is replaced with a float it works:
let add (x : {v:float|v>0} ) (y : {v:float|v>0} ) : { v:float | v >= x && v >= y} = let z = x +. y in zThe issue is that MARVeLus has no type inference mechanism to determine the type of z, which then default to float. When assigning "z = x + y" in Z3, it implicitly creates a new float x and a new float y, which then breaks the system.