# Why am I getting unsolved constraint?

**URL:** <https://discourse.ats-lang.org/t/why-am-i-getting-unsolved-constraint/352>\
**Category:** Google Group\
**Created:** [January 31, 2014, 11:45am UTC](https://discourse.ats-lang.org/t/why-am-i-getting-unsolved-constraint/352 "2014-01-31T11:45:31Z")\
**Posts on this page:** 13\
**Page:** 1

<div class="post-metadata">

**Author:** ![Chotu\_S](https://avatars.discourse-cdn.com/v4/letter/c/7cd45c/32.png) [@Chotu\_S](https://discourse.ats-lang.org/u/Chotu_S)\
**Post date:** [January 31, 2014, 11:45am UTC](https://discourse.ats-lang.org/t/why-am-i-getting-unsolved-constraint/352/1 "2014-01-31T11:45:31Z")

</div>

Hello,

Maybe I am missing some thing here(I am pretty sure 🙂 ) , may I know  
why is compiler asking for following constraint to be unsolved (rgt - 1) \>=  
0 . (I believe this is what it is asking)

Here is the code :

fun just\_a\_test {rgt : int} {lft : nat | lft \<= rgt+1}  
(left : int (lft) , right : int (rgt)) : [lft == rgt+1] void =  
if (left \<= right)  
then just\_a\_test{lft}{rgt-1} (left,right-1)  
else ()

Is there any counter example that makes above formulation impossible.

Thanks

---

<div class="post-metadata">

**Author:** ![Chotu\_S](https://avatars.discourse-cdn.com/v4/letter/c/7cd45c/32.png) [@Chotu\_S](https://discourse.ats-lang.org/u/Chotu_S)\
**Post date:** [January 31, 2014, 1:55pm UTC](https://discourse.ats-lang.org/t/why-am-i-getting-unsolved-constraint/352/2 "2014-01-31T13:55:14Z")

</div>

Brandon , what I am trying to do is my inputs have relationship l \<= r + 1  
where l is a nat and r is a int and I want to ensure that result of my  
function have property l==r+1.

Here is another example code of what I am trying to do :

#include “share/atspre\_define.hats”  
#include “share/atspre\_staload.hats”

val () = println! (“rough”)

(\* l must always be \>= 0 and return value must always have  
following relation : l == r+1 _)  
(_ this function assumes that inputs are l \>= 0 and l \<= r+1 \*)  
fun just\_a\_test2 (l : int , r : int) : (int,int) = let  
val () = assertloc (l \>= 0 && l \<= r+1)  
in  
if l \<= r  
then just\_a\_test2(l , r-1)  
else (l,r)  
end

val l = just\_a\_test2(0,10)  
val l2 = just\_a\_test2(0,~1)

val () = println! (l.0 , “,” , l.1)  
val () = println! (l2.0 , “,” , l2.1)

//val l3 = just\_a\_test2(0,~2) // this is invalid input and should fail

implement main0 () = ()On Friday, January 31, 2014 7:00:26 PM UTC+5:30, Brandon Barker wrote:

> fun just\_a\_test {rgt : int} {lft : nat | lft \<= rgt+1}  
> (left : int (lft) , right : int (rgt)) : [lft == rgt+1] void =  
> if (left \<= right)  
> then just\_a\_test (left, right+1)  
> else ()
> 
> >

---

<div class="post-metadata">

**Author:** ![Chotu\_S](https://avatars.discourse-cdn.com/v4/letter/c/7cd45c/32.png) [@Chotu\_S](https://discourse.ats-lang.org/u/Chotu_S)\
**Post date:** [January 31, 2014, 3:18pm UTC](https://discourse.ats-lang.org/t/why-am-i-getting-unsolved-constraint/352/3 "2014-01-31T15:18:04Z")

</div>

Ha ! , now I get it(I hope 🙂 ) , indeed I was mixing functional and  
imperative .

ThanksOn Friday, January 31, 2014 8:18:33 PM UTC+5:30, gmhwxi wrote:

> First, the quantifiers should probably be written as follows:
> 
> fun just\_a\_test  
> {lft:nat}{rgt : int | lft \<= rgt+1}  
> (left : int (lft) , right : int (rgt)) : [lft == rgt+1] void =  
> if (left \<= right)  
> then just\_a\_test{lft}{rgt-1} (left,right-1)  
> else ()
> 
> You are mixing functional programming with imperative programming.
> 
> Note that lft and rgt are fixed integers that cannot change during the  
> call.
> 
> On Friday, January 31, 2014 6:45:31 AM UTC-5, chotu s wrote:
> 
> > Hello,
> > 
> > Maybe I am missing some thing here(I am pretty sure 🙂 ) , may I know  
> > why is compiler asking for following constraint to be unsolved (rgt - 1) \>=  
> > 0 . (I believe this is what it is asking)
> > 
> > Here is the code :
> > 
> > fun just\_a\_test {rgt : int} {lft : nat | lft \<= rgt+1}  
> > (left : int (lft) , right : int (rgt)) : [lft == rgt+1] void =  
> > if (left \<= right)  
> > then just\_a\_test{lft}{rgt-1} (left,right-1)  
> > else ()
> > 
> > Is there any counter example that makes above formulation impossible.
> > 
> > Thanks

---

<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:** [January 31, 2014, 2:48pm UTC](https://discourse.ats-lang.org/t/why-am-i-getting-unsolved-constraint/352/4 "2014-01-31T14:48:33Z")

</div>

First, the quantifiers should probably be written as follows:

fun just\_a\_test  
{lft:nat}{rgt : int | lft \<= rgt+1}  
(left : int (lft) , right : int (rgt)) : [lft == rgt+1] void =  
if (left \<= right)  
then just\_a\_test{lft}{rgt-1} (left,right-1)  
else ()

You are mixing functional programming with imperative programming.

Note that lft and rgt are fixed integers that cannot change during the call.On Friday, January 31, 2014 6:45:31 AM UTC-5, chotu s wrote:

> Hello,
> 
> Maybe I am missing some thing here(I am pretty sure 🙂 ) , may I know  
> why is compiler asking for following constraint to be unsolved (rgt - 1) \>=  
> 0 . (I believe this is what it is asking)
> 
> Here is the code :
> 
> fun just\_a\_test {rgt : int} {lft : nat | lft \<= rgt+1}  
> (left : int (lft) , right : int (rgt)) : [lft == rgt+1] void =  
> if (left \<= right)  
> then just\_a\_test{lft}{rgt-1} (left,right-1)  
> else ()
> 
> Is there any counter example that makes above formulation impossible.
> 
> Thanks

---

<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:** [January 31, 2014, 3:25pm UTC](https://discourse.ats-lang.org/t/why-am-i-getting-unsolved-constraint/352/5 "2014-01-31T15:25:41Z")

</div>

This implementation is of imperative style:

fun just\_a\_test  
{lft:nat}{rgt : int | lft \<= rgt+1}  
(left : int (lft) , right : &int (rgt) \>\> int (lft-1)): void =  
(  
if (left \<= right)  
then (right := right-1; just\_a\_test (left, right))  
else ()  
// end of [if]  
)On Friday, January 31, 2014 10:12:51 AM UTC-5, Brandon Barker wrote:

> I’m curious what part of this is considered imperative programming?
> 
> Brandon Barker  
> [brand...@gmail.com](mailto:brand...@gmail.com) \<javascript:\>
> 
> On Fri, Jan 31, 2014 at 9:48 AM, gmhwxi \<[gmh...@gmail.com](mailto:gmh...@gmail.com) \<javascript:\>\>wrote:
> 
> > First, the quantifiers should probably be written as follows:
> > 
> > fun just\_a\_test  
> > {lft:nat}{rgt : int | lft \<= rgt+1}
> > 
> > (left : int (lft) , right : int (rgt)) : [lft == rgt+1] void =  
> > if (left \<= right)  
> > then just\_a\_test{lft}{rgt-1} (left,right-1)  
> > else ()
> > 
> > You are mixing functional programming with imperative programming.
> > 
> > Note that lft and rgt are fixed integers that cannot change during the  
> > call.
> > 
> > On Friday, January 31, 2014 6:45:31 AM UTC-5, chotu s wrote:
> > 
> > > Hello,
> > > 
> > > Maybe I am missing some thing here(I am pretty sure 🙂 ) , may I know  
> > > why is compiler asking for following constraint to be unsolved (rgt - 1) \>=  
> > > 0 . (I believe this is what it is asking)
> > > 
> > > Here is the code :
> > > 
> > > fun just\_a\_test {rgt : int} {lft : nat | lft \<= rgt+1}  
> > > (left : int (lft) , right : int (rgt)) : [lft == rgt+1] void =  
> > > if (left \<= right)  
> > > then just\_a\_test{lft}{rgt-1} (left,right-1)  
> > > else ()
> > > 
> > > Is there any counter example that makes above formulation impossible.
> > > 
> > > Thanks
> > > 
> > > –  
> > > 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...@googlegroups.com](mailto:ats-lang...@googlegroups.com) \<javascript:\>.  
> > > To post to this group, send email to [ats-l...@googlegroups.com](mailto:ats-l...@googlegroups.com)\<javascript:\>  
> > > .  
> > > To view this discussion on the web visit  
> > > [https://groups.google.com/d/msgid/ats-lang-users/47ad10de-0c3b-46b0-954f-19634d5eb2d3%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/47ad10de-0c3b-46b0-954f-19634d5eb2d3%40googlegroups.com)  
> > > .

---

<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:** [January 31, 2014, 2:52pm UTC](https://discourse.ats-lang.org/t/why-am-i-getting-unsolved-constraint/352/6 "2014-01-31T14:52:30Z")

</div>

The following function typechecks:

fun just\_a\_test  
{lft:nat}{rgt : int | lft \<= rgt+1}  
(left : int (lft) , right : int (rgt)) : [rgt:int | lft == rgt+1] int(rgt  
) =  
if (left \<= right)  
then just\_a\_test{lft}{rgt-1} (left,right-1)  
else right

Only ‘right’ needs to be returned as ‘left’ stays the same.On Friday, January 31, 2014 6:45:31 AM UTC-5, chotu s wrote:

> Hello,
> 
> Maybe I am missing some thing here(I am pretty sure 🙂 ) , may I know  
> why is compiler asking for following constraint to be unsolved (rgt - 1) \>=  
> 0 . (I believe this is what it is asking)
> 
> Here is the code :
> 
> fun just\_a\_test {rgt : int} {lft : nat | lft \<= rgt+1}  
> (left : int (lft) , right : int (rgt)) : [lft == rgt+1] void =  
> if (left \<= right)  
> then just\_a\_test{lft}{rgt-1} (left,right-1)  
> else ()
> 
> Is there any counter example that makes above formulation impossible.
> 
> Thanks

---

<div class="post-metadata">

**Author:** ![Brandon\_Barker](https://sea1.discourse-cdn.com/flex019/user_avatar/discourse.ats-lang.org/brandon_barker/32/61_2.png) [@Brandon\_Barker](https://discourse.ats-lang.org/u/Brandon_Barker)\
**Post date:** [January 31, 2014, 2:13pm UTC](https://discourse.ats-lang.org/t/why-am-i-getting-unsolved-constraint/352/7 "2014-01-31T14:13:42Z")

</div>

How about this? You need a new static variable (rgt\_out) for the right  
variable that is being output, as it changes over the course of execution.

fun just\_a\_test {rgt : int} {lft : nat | lft \<= rgt + 1}  
(left : int (lft) , right : int (rgt)  
) : [rgt\_out : int | lft == rgt\_out + 1] (int lft, int rgt\_out) =  
if (left = (right + 1)) then (left, right)  
else just\_a\_test (left,right-1)On Friday, January 31, 2014 8:55:14 AM UTC-5, chotu s wrote:

> Brandon , what I am trying to do is my inputs have relationship l \<= r +  
> 1 where l is a nat and r is a int and I want to ensure that result of my  
> function have property l==r+1.
> 
> Here is another example code of what I am trying to do :
> 
> #include “share/atspre\_define.hats”  
> #include “share/atspre\_staload.hats”
> 
> val () = println! (“rough”)
> 
> (\* l must always be \>= 0 and return value must always have  
> following relation : l == r+1 _)  
> (_ this function assumes that inputs are l \>= 0 and l \<= r+1 \*)  
> fun just\_a\_test2 (l : int , r : int) : (int,int) = let  
> val () = assertloc (l \>= 0 && l \<= r+1)  
> in  
> if l \<= r  
> then just\_a\_test2(l , r-1)  
> else (l,r)  
> end
> 
> val l = just\_a\_test2(0,10)  
> val l2 = just\_a\_test2(0,~1)
> 
> val () = println! (l.0 , “,” , l.1)  
> val () = println! (l2.0 , “,” , l2.1)
> 
> //val l3 = just\_a\_test2(0,~2) // this is invalid input and should fail
> 
> implement main0 () = ()
> 
> On Friday, January 31, 2014 7:00:26 PM UTC+5:30, Brandon Barker wrote:
> 
> > fun just\_a\_test {rgt : int} {lft : nat | lft \<= rgt+1}  
> > (left : int (lft) , right : int (rgt)) : [lft == rgt+1] void =  
> > if (left \<= right)  
> > then just\_a\_test (left, right+1)  
> > else ()
> > 
> > >

---

<div class="post-metadata">

**Author:** ![Brandon\_Barker](https://sea1.discourse-cdn.com/flex019/user_avatar/discourse.ats-lang.org/brandon_barker/32/61_2.png) [@Brandon\_Barker](https://discourse.ats-lang.org/u/Brandon_Barker)\
**Post date:** [January 31, 2014, 3:12pm UTC](https://discourse.ats-lang.org/t/why-am-i-getting-unsolved-constraint/352/8 "2014-01-31T15:12:51Z")

</div>

I’m curious what part of this is considered imperative programming?

Brandon Barker  
brandon…@gmail.comOn Fri, Jan 31, 2014 at 9:48 AM, gmhwxi [gmh...@gmail.com](mailto:gmh...@gmail.com) wrote:

> First, the quantifiers should probably be written as follows:
> 
> fun just\_a\_test  
> {lft:nat}{rgt : int | lft \<= rgt+1}
> 
> (left : int (lft) , right : int (rgt)) : [lft == rgt+1] void =  
> if (left \<= right)  
> then just\_a\_test{lft}{rgt-1} (left,right-1)  
> else ()
> 
> You are mixing functional programming with imperative programming.
> 
> Note that lft and rgt are fixed integers that cannot change during the  
> call.
> 
> On Friday, January 31, 2014 6:45:31 AM UTC-5, chotu s wrote:
> 
> > Hello,
> > 
> > Maybe I am missing some thing here(I am pretty sure 🙂 ) , may I know  
> > why is compiler asking for following constraint to be unsolved (rgt - 1) \>=  
> > 0 . (I believe this is what it is asking)
> > 
> > Here is the code :
> > 
> > fun just\_a\_test {rgt : int} {lft : nat | lft \<= rgt+1}  
> > (left : int (lft) , right : int (rgt)) : [lft == rgt+1] void =  
> > if (left \<= right)  
> > then just\_a\_test{lft}{rgt-1} (left,right-1)  
> > else ()
> > 
> > Is there any counter example that makes above formulation impossible.
> > 
> > Thanks
> > 
> > –  
> > 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/47ad10de-0c3b-46b0-954f-19634d5eb2d3%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/47ad10de-0c3b-46b0-954f-19634d5eb2d3%40googlegroups.com)  
> > .

---

<div class="post-metadata">

**Author:** ![Chotu\_S](https://avatars.discourse-cdn.com/v4/letter/c/7cd45c/32.png) [@Chotu\_S](https://discourse.ats-lang.org/u/Chotu_S)\
**Post date:** [January 31, 2014, 3:48pm UTC](https://discourse.ats-lang.org/t/why-am-i-getting-unsolved-constraint/352/9 "2014-01-31T15:48:00Z")

</div>

Another stupid mistake I did not realize was that order {lft}{rgt-1}was  
also incorrect as per function spec :(On Friday, January 31, 2014 5:15:31 PM UTC+5:30, chotu s wrote:

> Hello,
> 
> Maybe I am missing some thing here(I am pretty sure 🙂 ) , may I know  
> why is compiler asking for following constraint to be unsolved (rgt - 1) \>=  
> 0 . (I believe this is what it is asking)
> 
> Here is the code :
> 
> fun just\_a\_test {rgt : int} {lft : nat | lft \<= rgt+1}  
> (left : int (lft) , right : int (rgt)) : [lft == rgt+1] void =  
> if (left \<= right)  
> then just\_a\_test{lft}{rgt-1} (left,right-1)  
> else ()
> 
> Is there any counter example that makes above formulation impossible.
> 
> Thanks

---

<div class="post-metadata">

**Author:** ![Brandon\_Barker](https://sea1.discourse-cdn.com/flex019/user_avatar/discourse.ats-lang.org/brandon_barker/32/61_2.png) [@Brandon\_Barker](https://discourse.ats-lang.org/u/Brandon_Barker)\
**Post date:** [January 31, 2014, 3:16pm UTC](https://discourse.ats-lang.org/t/why-am-i-getting-unsolved-constraint/352/10 "2014-01-31T15:16:40Z")

</div>

Sorry, nevermind: I guess it is because only the void is being returned;  
but it seems to have no effects, so I thought it was functional.

Brandon Barker  
brandon…@gmail.comOn Fri, Jan 31, 2014 at 10:12 AM, Brandon Barker [brandon...@gmail.com](mailto:brandon...@gmail.com)wrote:

> I’m curious what part of this is considered imperative programming?
> 
> Brandon Barker  
> [brandon...@gmail.com](mailto:brandon...@gmail.com)
> 
> On Fri, Jan 31, 2014 at 9:48 AM, gmhwxi [gmh...@gmail.com](mailto:gmh...@gmail.com) wrote:
> 
> > First, the quantifiers should probably be written as follows:
> > 
> > fun just\_a\_test  
> > {lft:nat}{rgt : int | lft \<= rgt+1}
> > 
> > (left : int (lft) , right : int (rgt)) : [lft == rgt+1] void =  
> > if (left \<= right)  
> > then just\_a\_test{lft}{rgt-1} (left,right-1)  
> > else ()
> > 
> > You are mixing functional programming with imperative programming.
> > 
> > Note that lft and rgt are fixed integers that cannot change during the  
> > call.
> > 
> > On Friday, January 31, 2014 6:45:31 AM UTC-5, chotu s wrote:
> > 
> > > Hello,
> > > 
> > > Maybe I am missing some thing here(I am pretty sure 🙂 ) , may I know  
> > > why is compiler asking for following constraint to be unsolved (rgt - 1) \>=  
> > > 0 . (I believe this is what it is asking)
> > > 
> > > Here is the code :
> > > 
> > > fun just\_a\_test {rgt : int} {lft : nat | lft \<= rgt+1}  
> > > (left : int (lft) , right : int (rgt)) : [lft == rgt+1] void =  
> > > if (left \<= right)  
> > > then just\_a\_test{lft}{rgt-1} (left,right-1)  
> > > else ()
> > > 
> > > Is there any counter example that makes above formulation impossible.
> > > 
> > > Thanks
> > > 
> > > –  
> > > 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/47ad10de-0c3b-46b0-954f-19634d5eb2d3%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/47ad10de-0c3b-46b0-954f-19634d5eb2d3%40googlegroups.com)  
> > > .

---

<div class="post-metadata">

**Author:** ![Brandon\_Barker](https://sea1.discourse-cdn.com/flex019/user_avatar/discourse.ats-lang.org/brandon_barker/32/61_2.png) [@Brandon\_Barker](https://discourse.ats-lang.org/u/Brandon_Barker)\
**Post date:** [January 31, 2014, 1:25pm UTC](https://discourse.ats-lang.org/t/why-am-i-getting-unsolved-constraint/352/11 "2014-01-31T13:25:07Z")

</div>

1: I don’t think you need just\_a\_test{lft}{rgt-1} in a call to a  
polymorphic function, just “just\_a\_test”.  
2: I htink your return type is wrong: if you change the recursive case  
to : (left,right+1), it works.  
Brandon Barker  
brandon…@gmail.comOn Fri, Jan 31, 2014 at 6:45 AM, chotu s [chot...@gmail.com](mailto:chot...@gmail.com) wrote:

> Hello,
> 
> Maybe I am missing some thing here(I am pretty sure 🙂 ) , may I know why  
> is compiler asking for following constraint to be unsolved (rgt - 1) \>= 0 .  
> (I believe this is what it is asking)
> 
> Here is the code :
> 
> fun just\_a\_test {rgt : int} {lft : nat | lft \<= rgt+1}  
> (left : int (lft) , right : int (rgt)) : [lft == rgt+1] void =  
> if (left \<= right)  
> then just\_a\_test{lft}{rgt-1} (left,right-1)  
> else ()
> 
> Is there any counter example that makes above formulation impossible.
> 
> Thanks
> 
> –  
> 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/4674e7ce-9d11-45ff-8d92-f36fa0c49322%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/4674e7ce-9d11-45ff-8d92-f36fa0c49322%40googlegroups.com).

---

<div class="post-metadata">

**Author:** ![Brandon\_Barker](https://sea1.discourse-cdn.com/flex019/user_avatar/discourse.ats-lang.org/brandon_barker/32/61_2.png) [@Brandon\_Barker](https://discourse.ats-lang.org/u/Brandon_Barker)\
**Post date:** [January 31, 2014, 1:30pm UTC](https://discourse.ats-lang.org/t/why-am-i-getting-unsolved-constraint/352/12 "2014-01-31T13:30:26Z")

</div>

fun just\_a\_test {rgt : int} {lft : nat | lft \<= rgt+1}  
(left : int (lft) , right : int (rgt)) : [lft == rgt+1] void =  
if (left \<= right)  
then just\_a\_test (left, right+1)  
else ()

---

<div class="post-metadata">

**Author:** ![Chotu\_S](https://avatars.discourse-cdn.com/v4/letter/c/7cd45c/32.png) [@Chotu\_S](https://discourse.ats-lang.org/u/Chotu_S)\
**Post date:** [January 31, 2014, 2:32pm UTC](https://discourse.ats-lang.org/t/why-am-i-getting-unsolved-constraint/352/13 "2014-01-31T14:32:26Z")

</div>

Thanks, yes this seems to work , let me try to plug it in actual program  
and see if it solves the issue . But I wonder why original code fragement  
does not work , is it not that linear constraints (which I presume it is )  
are solved by the compiler , I wonder if my original formulation wrong .On Friday, January 31, 2014 7:43:42 PM UTC+5:30, Brandon Barker wrote:

> How about this? You need a new static variable (rgt\_out) for the right  
> variable that is being output, as it changes over the course of execution.
> 
> fun just\_a\_test {rgt : int} {lft : nat | lft \<= rgt + 1}  
> (left : int (lft) , right : int (rgt)  
> ) : [rgt\_out : int | lft == rgt\_out + 1] (int lft, int rgt\_out) =  
> if (left = (right + 1)) then (left, right)  
> else just\_a\_test (left,right-1)
> 
> On Friday, January 31, 2014 8:55:14 AM UTC-5, chotu s wrote:
> 
> > Brandon , what I am trying to do is my inputs have relationship l \<= r +  
> > 1 where l is a nat and r is a int and I want to ensure that result of my  
> > function have property l==r+1.
> > 
> > Here is another example code of what I am trying to do :
> > 
> > #include “share/atspre\_define.hats”  
> > #include “share/atspre\_staload.hats”
> > 
> > val () = println! (“rough”)
> > 
> > (\* l must always be \>= 0 and return value must always have  
> > following relation : l == r+1 _)  
> > (_ this function assumes that inputs are l \>= 0 and l \<= r+1 \*)  
> > fun just\_a\_test2 (l : int , r : int) : (int,int) = let  
> > val () = assertloc (l \>= 0 && l \<= r+1)  
> > in  
> > if l \<= r  
> > then just\_a\_test2(l , r-1)  
> > else (l,r)  
> > end
> > 
> > val l = just\_a\_test2(0,10)  
> > val l2 = just\_a\_test2(0,~1)
> > 
> > val () = println! (l.0 , “,” , l.1)  
> > val () = println! (l2.0 , “,” , l2.1)
> > 
> > //val l3 = just\_a\_test2(0,~2) // this is invalid input and should fail
> > 
> > implement main0 () = ()
> > 
> > On Friday, January 31, 2014 7:00:26 PM UTC+5:30, Brandon Barker wrote:
> > 
> > > fun just\_a\_test {rgt : int} {lft : nat | lft \<= rgt+1}  
> > > (left : int (lft) , right : int (rgt)) : [lft == rgt+1] void =  
> > > if (left \<= right)  
> > > then just\_a\_test (left, right+1)  
> > > else ()
> > > 
> > > >