This is because the compiler does not know the product of two natural
numbers
is also a natural number.On Sun, Mar 30, 2014 at 3:40 AM, Shahab Tasharrofi < shahab.t...@gmail.com> wrote:
I still have a constraint in my program that does not pass constraint
solving
phase. The general way of the relevant part in my problem was similar to
the
factorial example and, so, I took the following factorial implementation
from
the ATS book and checked to see if it can pass the constraint solving. I
observed that factorial example below cannot pass the constraint solving
either.
fun fact {n:nat} (x: int n): [r:nat] int r = if x > 0 then x * fact (x-1)
else 1
While I cannot be sure if my problem and the problem with factorial example
above are indeed the same, I first want to see what the problem with the
above implementation is and then check if my problem is also the same.
fun
fact{n:nat}
(
x: int n
) : [r:nat] int r =
(
if x > 0
then let
val [r1:int] r1 = fact (x-1)
prval () = mul_gte_gte_gte {n,r1} ()
in
x * r1
end // end of [then]
else 1 // end of [else]
) (* end of [if] *)On Sunday, March 30, 2014 9:49:05 AM UTC-4, gmhwxi wrote:
This is because the compiler does not know the product of two natural
numbers
is also a natural number.
I still have a constraint in my program that does not pass constraint
solving
phase. The general way of the relevant part in my problem was similar to
the
factorial example and, so, I took the following factorial implementation
from
the ATS book and checked to see if it can pass the constraint solving. I
observed that factorial example below cannot pass the constraint solving
either.
fun fact {n:nat} (x: int n): [r:nat] int r = if x > 0 then x * fact (x-1)
else 1
While I cannot be sure if my problem and the problem with factorial
example
above are indeed the same, I first want to see what the problem with the
above implementation is and then check if my problem is also the same.