# Unsolved constraint in factorial example

**URL:** <https://discourse.ats-lang.org/t/unsolved-constraint-in-factorial-example/474>\
**Category:** Google Group\
**Created:** [March 30, 2014, 1:49pm UTC](https://discourse.ats-lang.org/t/unsolved-constraint-in-factorial-example/474 "2014-03-30T13:49:05Z")\
**Posts on this page:** 2\
**Page:** 1

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [March 30, 2014, 1:49pm UTC](https://discourse.ats-lang.org/t/unsolved-constraint-in-factorial-example/474/1 "2014-03-30T13:49:05Z")

</div>

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](mailto: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.
> 
> –  
> You received this message because you are subscribed to the Google Groups  
> “ats-lang-users” group.  
> To unsubscribe from this group and stop receiving emails from it, send an  
> email to [ats-lang-user...@googlegroups.com](mailto:ats-lang-user...@googlegroups.com).  
> To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> To view this discussion on the web visit  
> [https://groups.google.com/d/msgid/ats-lang-users/cb961436-c31d-4839-bf80-6891154d2bbd%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/cb961436-c31d-4839-bf80-6891154d2bbd%40googlegroups.com)[https://groups.google.com/d/msgid/ats-lang-users/cb961436-c31d-4839-bf80-6891154d2bbd%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/cb961436-c31d-4839-bf80-6891154d2bbd%40googlegroups.com?utm_medium=email&utm_source=footer)  
> .

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [March 30, 2014, 3:19pm UTC](https://discourse.ats-lang.org/t/unsolved-constraint-in-factorial-example/474/2 "2014-03-30T15:19:46Z")

</div>

Here is a version that type-checks:

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.
> 
> On Sun, Mar 30, 2014 at 3:40 AM, Shahab Tasharrofi \< [shahab.t...@gmail.com](mailto: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.
> > 
> > –  
> > You received this message because you are subscribed to the Google Groups  
> > “ats-lang-users” group.  
> > To unsubscribe from this group and stop receiving emails from it, send an  
> > email to [ats-lang-user...@googlegroups.com](mailto:ats-lang-user...@googlegroups.com).  
> > To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> > To view this discussion on the web visit  
> > [https://groups.google.com/d/msgid/ats-lang-users/cb961436-c31d-4839-bf80-6891154d2bbd%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/cb961436-c31d-4839-bf80-6891154d2bbd%40googlegroups.com)[https://groups.google.com/d/msgid/ats-lang-users/cb961436-c31d-4839-bf80-6891154d2bbd%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/cb961436-c31d-4839-bf80-6891154d2bbd%40googlegroups.com?utm_medium=email&utm_source=footer)  
> > .