# Weird Lemma In ATS Filter Function.b

**URL:** <https://discourse.ats-lang.org/t/weird-lemma-in-ats-filter-function-b/102>\
**Category:** Google Group\
**Created:** [August 7, 2015, 8:57pm UTC](https://discourse.ats-lang.org/t/weird-lemma-in-ats-filter-function-b/102 "2015-08-07T20:57:03Z")\
**Posts on this page:** 8\
**Page:** 1

<div class="post-metadata">

**Author:** ![aditya\_siram](https://avatars.discourse-cdn.com/v4/letter/a/b9e5f3/32.png) [@aditya\_siram](https://discourse.ats-lang.org/u/aditya_siram)\
**Post date:** [August 7, 2015, 8:57pm UTC](https://discourse.ats-lang.org/t/weird-lemma-in-ats-filter-function-b/102/1 "2015-08-07T20:57:03Z")

</div>

Hi all,  
I recently gave a talk on ATS  
\*[https://github.com/deech/ATSPresentation/blob/master/presentation.org](https://github.com/deech/ATSPresentation/blob/master/presentation.org)) and  
attempted to write a function that filtered a linear polymorphic list:  
[https://github.com/deech/ATSPresentation/blob/master/filter\_list.dats#L5](https://github.com/deech/ATSPresentation/blob/master/filter_list.dats#L5).

Without the line:  
[https://github.com/deech/ATSPresentation/blob/master/filter\_list.dats#L16](https://github.com/deech/ATSPresentation/blob/master/filter_list.dats#L16),  
I got this constraint error:  
  
"/home/deech/Downloads/ATS2-Postiats-0.2.1"/bin/patscc  
-DATS\_MEMALLOC\_LIBC -O2 -flto -o filter\_list filter\_list.dats || echo  
filter\_list “: ERROR!!!”  
/home/deech/ATS/ATSPresentation/filter\_list.dats: 432(line=16, offs=30) –  
432(line=16, offs=30): error(3): unsolved constraint:  
C3NSTRprop(C3TKmain(); S2Eapp(S2Ecst(\>=);  
S2EVar(4410-\>S2Evar(k$7234$7235$7236(12754))), S2Eintinf(0)))  
typechecking has failed: there are some unsolved constraints: please  
inspect the above reported error message(s) for information.  
exit(ATS): uncaught exception:  
\_2home\_2hwxi\_2research\_2Postiats\_2git\_2src\_2pats\_error\_2esats\_\_FatalErrorExn(1025)  
filter\_list : ERROR!!!

It seems to be asking for proof that some number ( which I assume to be the  
length of the rest of the list ) is \>= 0 but I’m not sure why. Can anyone  
explain?

Thanks!  
-deech

---

<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:** [August 8, 2015, 1:08am UTC](https://discourse.ats-lang.org/t/weird-lemma-in-ats-filter-function-b/102/2 "2015-08-08T01:08:30Z")

</div>

I tidied up the code a bit. See:

> <https://github.com/githwxi/ATS-Postiats-test/blob/master/core/MISC/test06.dats>

If you change [k: int | k \<= n] to [k: nat | k \<= n], then the lemma is not  
needed.  
The need for the lemma is due to list\_vt\_cons requiring its second argument  
to be  
a list of non-negative length. Yes, every length is non-negative, but the  
typechecker  
of ATS does not know this fact.

The tail-call in the filter function is not eliminated. I will fix this  
issue in the next release  
of ATS. For now, if you want the tail-call to be eliminated, please use the  
following coding  
style:

extern fun list\_vt\_filter …  
implement{a} list\_vt\_filter (xs, f) = …On Friday, August 7, 2015 at 4:57:03 PM UTC-4, aditya siram wrote:

> Hi all,  
> I recently gave a talk on ATS \*  
> [https://github.com/deech/ATSPresentation/blob/master/presentation.org](https://github.com/deech/ATSPresentation/blob/master/presentation.org))  
> and attempted to write a function that filtered a linear polymorphic list:  
> [https://github.com/deech/ATSPresentation/blob/master/filter\_list.dats#L5](https://github.com/deech/ATSPresentation/blob/master/filter_list.dats#L5).
> 
> Without the line:  
> [https://github.com/deech/ATSPresentation/blob/master/filter\_list.dats#L16](https://github.com/deech/ATSPresentation/blob/master/filter_list.dats#L16),  
> I got this constraint error:  
>   
> “/home/deech/Downloads/ATS2-Postiats-0.2.1”/bin/patscc  
> -DATS\_MEMALLOC\_LIBC -O2 -flto -o filter\_list filter\_list.dats || echo  
> filter\_list “: ERROR!!!”  
> /home/deech/ATS/ATSPresentation/filter\_list.dats: 432(line=16, offs=30) –  
> 432(line=16, offs=30): error(3): unsolved constraint:  
> C3NSTRprop(C3TKmain(); S2Eapp(S2Ecst(\>=);  
> S2EVar(4410-\>S2Evar(k$7234$7235$7236(12754))), S2Eintinf(0)))  
> typechecking has failed: there are some unsolved constraints: please  
> inspect the above reported error message(s) for information.  
> exit(ATS): uncaught exception:  
> \_2home\_2hwxi\_2research\_2Postiats\_2git\_2src\_2pats\_error\_2esats\_\_FatalErrorExn(1025)  
> filter\_list : ERROR!!!
> 
> It seems to be asking for proof that some number ( which I assume to be  
> the length of the rest of the list ) is \>= 0 but I’m not sure why. Can  
> anyone explain?
> 
> Thanks!  
> -deech

---

<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:** [August 8, 2015, 1:54am UTC](https://discourse.ats-lang.org/t/weird-lemma-in-ats-filter-function-b/102/3 "2015-08-08T01:54:33Z")

</div>

‘nat’ is not a regular sort; it is a so-called subset sort:

sortdef nat = {a: int | a \>= 0}

Type constructors in ATS are only allowed to be parametrized over regular  
sorts  
such as int, bool, type, t0ype, vtype, vt0ype, prop, view, and user-defined  
datasorts.

The kind of list type you have in mind can essentially be defined as  
follows:

typedef list\_nonnegative(a:t0ype, n:int) = [n \> 0] list(a, n)On Friday, August 7, 2015 at 9:44:34 PM UTC-4, aditya siram wrote:

> Ah! That makes sense. Thanks!
> 
> I guess my follow-up question would be, why are all the list lengths in  
> “./prelude/SATS/list\_vt.sats” parameterized with sort `int`? I guess the  
> type constructors don’t allow constructing a list\_vt with a negative length  
> but all the same I would have expected it to be sort `nat`.
> 
> -deech
> 
> On Friday, August 7, 2015 at 8:08:31 PM UTC-5, gmhwxi wrote:
> 
> > I tidied up the code a bit. See:
> > 
> > [https://github.com/githwxi/ATS-Postiats-test/blob/master/core/MISC/test06.dats](https://github.com/githwxi/ATS-Postiats-test/blob/master/core/MISC/test06.dats)
> > 
> > If you change [k: int | k \<= n] to [k: nat | k \<= n], then the lemma is  
> > not needed.  
> > The need for the lemma is due to list\_vt\_cons requiring its second  
> > argument to be  
> > a list of non-negative length. Yes, every length is non-negative, but the  
> > typechecker  
> > of ATS does not know this fact.
> > 
> > The tail-call in the filter function is not eliminated. I will fix this  
> > issue in the next release  
> > of ATS. For now, if you want the tail-call to be eliminated, please use  
> > the following coding  
> > style:
> > 
> > extern fun list\_vt\_filter …  
> > implement{a} list\_vt\_filter (xs, f) = …
> > 
> > On Friday, August 7, 2015 at 4:57:03 PM UTC-4, aditya siram wrote:
> > 
> > > Hi all,  
> > > I recently gave a talk on ATS \*  
> > > [https://github.com/deech/ATSPresentation/blob/master/presentation.org](https://github.com/deech/ATSPresentation/blob/master/presentation.org))  
> > > and attempted to write a function that filtered a linear polymorphic list:  
> > > [https://github.com/deech/ATSPresentation/blob/master/filter\_list.dats#L5](https://github.com/deech/ATSPresentation/blob/master/filter_list.dats#L5).
> > > 
> > > Without the line:  
> > > [https://github.com/deech/ATSPresentation/blob/master/filter\_list.dats#L16](https://github.com/deech/ATSPresentation/blob/master/filter_list.dats#L16),  
> > > I got this constraint error:  
> > >   
> > > “/home/deech/Downloads/ATS2-Postiats-0.2.1”/bin/patscc  
> > > -DATS\_MEMALLOC\_LIBC -O2 -flto -o filter\_list filter\_list.dats || echo  
> > > filter\_list “: ERROR!!!”  
> > > /home/deech/ATS/ATSPresentation/filter\_list.dats: 432(line=16, offs=30)  
> > > – 432(line=16, offs=30): error(3): unsolved constraint:  
> > > C3NSTRprop(C3TKmain(); S2Eapp(S2Ecst(\>=);  
> > > S2EVar(4410-\>S2Evar(k$7234$7235$7236(12754))), S2Eintinf(0)))  
> > > typechecking has failed: there are some unsolved constraints: please  
> > > inspect the above reported error message(s) for information.  
> > > exit(ATS): uncaught exception:  
> > > \_2home\_2hwxi\_2research\_2Postiats\_2git\_2src\_2pats\_error\_2esats\_\_FatalErrorExn(1025)  
> > > filter\_list : ERROR!!!
> > > 
> > > It seems to be asking for proof that some number ( which I assume to be  
> > > the length of the rest of the list ) is \>= 0 but I’m not sure why. Can  
> > > anyone explain?
> > > 
> > > Thanks!  
> > > -deech

---

<div class="post-metadata">

**Author:** ![aditya\_siram](https://avatars.discourse-cdn.com/v4/letter/a/b9e5f3/32.png) [@aditya\_siram](https://discourse.ats-lang.org/u/aditya_siram)\
**Post date:** [August 7, 2015, 9:00pm UTC](https://discourse.ats-lang.org/t/weird-lemma-in-ats-filter-function-b/102/4 "2015-08-07T21:00:38Z")

</div>

Also I was wondering if the tail call in the filter function was eliminated  
by the compiler. The ATS book seems to indicate that it is but I wanted to  
verify.

Thanks!  
-deechOn Friday, August 7, 2015 at 3:57:03 PM UTC-5, aditya siram wrote:

> Hi all,  
> I recently gave a talk on ATS \*  
> [https://github.com/deech/ATSPresentation/blob/master/presentation.org](https://github.com/deech/ATSPresentation/blob/master/presentation.org))  
> and attempted to write a function that filtered a linear polymorphic list:  
> [https://github.com/deech/ATSPresentation/blob/master/filter\_list.dats#L5](https://github.com/deech/ATSPresentation/blob/master/filter_list.dats#L5).
> 
> Without the line:  
> [https://github.com/deech/ATSPresentation/blob/master/filter\_list.dats#L16](https://github.com/deech/ATSPresentation/blob/master/filter_list.dats#L16),  
> I got this constraint error:  
>   
> “/home/deech/Downloads/ATS2-Postiats-0.2.1”/bin/patscc  
> -DATS\_MEMALLOC\_LIBC -O2 -flto -o filter\_list filter\_list.dats || echo  
> filter\_list “: ERROR!!!”  
> /home/deech/ATS/ATSPresentation/filter\_list.dats: 432(line=16, offs=30) –  
> 432(line=16, offs=30): error(3): unsolved constraint:  
> C3NSTRprop(C3TKmain(); S2Eapp(S2Ecst(\>=);  
> S2EVar(4410-\>S2Evar(k$7234$7235$7236(12754))), S2Eintinf(0)))  
> typechecking has failed: there are some unsolved constraints: please  
> inspect the above reported error message(s) for information.  
> exit(ATS): uncaught exception:  
> \_2home\_2hwxi\_2research\_2Postiats\_2git\_2src\_2pats\_error\_2esats\_\_FatalErrorExn(1025)  
> filter\_list : ERROR!!!
> 
> It seems to be asking for proof that some number ( which I assume to be  
> the length of the rest of the list ) is \>= 0 but I’m not sure why. Can  
> anyone explain?
> 
> Thanks!  
> -deech

---

<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:** [August 8, 2015, 1:55am UTC](https://discourse.ats-lang.org/t/weird-lemma-in-ats-filter-function-b/102/5 "2015-08-08T01:55:44Z")

</div>

Should be:

typedef list\_nonnegative(a:t0ype, n:int) = [n \>= 0] list(a, n)On Friday, August 7, 2015 at 9:54:33 PM UTC-4, gmhwxi wrote:

> ‘nat’ is not a regular sort; it is a so-called subset sort:
> 
> sortdef nat = {a: int | a \>= 0}
> 
> Type constructors in ATS are only allowed to be parametrized over regular  
> sorts  
> such as int, bool, type, t0ype, vtype, vt0ype, prop, view, and  
> user-defined datasorts.
> 
> The kind of list type you have in mind can essentially be defined as  
> follows:
> 
> typedef list\_nonnegative(a:t0ype, n:int) = [n \> 0] list(a, n)
> 
> On Friday, August 7, 2015 at 9:44:34 PM UTC-4, aditya siram wrote:
> 
> > Ah! That makes sense. Thanks!
> > 
> > I guess my follow-up question would be, why are all the list lengths in  
> > “./prelude/SATS/list\_vt.sats” parameterized with sort `int`? I guess the  
> > type constructors don’t allow constructing a list\_vt with a negative length  
> > but all the same I would have expected it to be sort `nat`.
> > 
> > -deech
> > 
> > On Friday, August 7, 2015 at 8:08:31 PM UTC-5, gmhwxi wrote:
> > 
> > > I tidied up the code a bit. See:
> > > 
> > > [https://github.com/githwxi/ATS-Postiats-test/blob/master/core/MISC/test06.dats](https://github.com/githwxi/ATS-Postiats-test/blob/master/core/MISC/test06.dats)
> > > 
> > > If you change [k: int | k \<= n] to [k: nat | k \<= n], then the lemma is  
> > > not needed.  
> > > The need for the lemma is due to list\_vt\_cons requiring its second  
> > > argument to be  
> > > a list of non-negative length. Yes, every length is non-negative, but  
> > > the typechecker  
> > > of ATS does not know this fact.
> > > 
> > > The tail-call in the filter function is not eliminated. I will fix this  
> > > issue in the next release  
> > > of ATS. For now, if you want the tail-call to be eliminated, please use  
> > > the following coding  
> > > style:
> > > 
> > > extern fun list\_vt\_filter …  
> > > implement{a} list\_vt\_filter (xs, f) = …
> > > 
> > > On Friday, August 7, 2015 at 4:57:03 PM UTC-4, aditya siram wrote:
> > > 
> > > > Hi all,  
> > > > I recently gave a talk on ATS \*  
> > > > [https://github.com/deech/ATSPresentation/blob/master/presentation.org](https://github.com/deech/ATSPresentation/blob/master/presentation.org))  
> > > > and attempted to write a function that filtered a linear polymorphic list:  
> > > > [https://github.com/deech/ATSPresentation/blob/master/filter\_list.dats#L5](https://github.com/deech/ATSPresentation/blob/master/filter_list.dats#L5).
> > > > 
> > > > Without the line:  
> > > > [https://github.com/deech/ATSPresentation/blob/master/filter\_list.dats#L16](https://github.com/deech/ATSPresentation/blob/master/filter_list.dats#L16),  
> > > > I got this constraint error:  
> > > >   
> > > > “/home/deech/Downloads/ATS2-Postiats-0.2.1”/bin/patscc  
> > > > -DATS\_MEMALLOC\_LIBC -O2 -flto -o filter\_list filter\_list.dats || echo  
> > > > filter\_list “: ERROR!!!”  
> > > > /home/deech/ATS/ATSPresentation/filter\_list.dats: 432(line=16, offs=30)  
> > > > – 432(line=16, offs=30): error(3): unsolved constraint:  
> > > > C3NSTRprop(C3TKmain(); S2Eapp(S2Ecst(\>=);  
> > > > S2EVar(4410-\>S2Evar(k$7234$7235$7236(12754))), S2Eintinf(0)))  
> > > > typechecking has failed: there are some unsolved constraints: please  
> > > > inspect the above reported error message(s) for information.  
> > > > exit(ATS): uncaught exception:  
> > > > \_2home\_2hwxi\_2research\_2Postiats\_2git\_2src\_2pats\_error\_2esats\_\_FatalErrorExn(1025)  
> > > > filter\_list : ERROR!!!
> > > > 
> > > > It seems to be asking for proof that some number ( which I assume to be  
> > > > the length of the rest of the list ) is \>= 0 but I’m not sure why. Can  
> > > > anyone explain?
> > > > 
> > > > Thanks!  
> > > > -deech

---

<div class="post-metadata">

**Author:** ![aditya\_siram](https://avatars.discourse-cdn.com/v4/letter/a/b9e5f3/32.png) [@aditya\_siram](https://discourse.ats-lang.org/u/aditya_siram)\
**Post date:** [August 8, 2015, 1:44am UTC](https://discourse.ats-lang.org/t/weird-lemma-in-ats-filter-function-b/102/6 "2015-08-08T01:44:34Z")

</div>

Ah! That makes sense. Thanks!

I guess my follow-up question would be, why are all the list lengths in  
“./prelude/SATS/list\_vt.sats” parameterized with sort `int`? I guess the  
type constructors don’t allow constructing a list\_vt with a negative length  
but all the same I would have expected it to be sort `nat`.

-deechOn Friday, August 7, 2015 at 8:08:31 PM UTC-5, gmhwxi wrote:

> I tidied up the code a bit. See:
> 
> [https://github.com/githwxi/ATS-Postiats-test/blob/master/core/MISC/test06.dats](https://github.com/githwxi/ATS-Postiats-test/blob/master/core/MISC/test06.dats)
> 
> If you change [k: int | k \<= n] to [k: nat | k \<= n], then the lemma is  
> not needed.  
> The need for the lemma is due to list\_vt\_cons requiring its second  
> argument to be  
> a list of non-negative length. Yes, every length is non-negative, but the  
> typechecker  
> of ATS does not know this fact.
> 
> The tail-call in the filter function is not eliminated. I will fix this  
> issue in the next release  
> of ATS. For now, if you want the tail-call to be eliminated, please use  
> the following coding  
> style:
> 
> extern fun list\_vt\_filter …  
> implement{a} list\_vt\_filter (xs, f) = …
> 
> On Friday, August 7, 2015 at 4:57:03 PM UTC-4, aditya siram wrote:
> 
> > Hi all,  
> > I recently gave a talk on ATS \*  
> > [https://github.com/deech/ATSPresentation/blob/master/presentation.org](https://github.com/deech/ATSPresentation/blob/master/presentation.org))  
> > and attempted to write a function that filtered a linear polymorphic list:  
> > [https://github.com/deech/ATSPresentation/blob/master/filter\_list.dats#L5](https://github.com/deech/ATSPresentation/blob/master/filter_list.dats#L5).
> > 
> > Without the line:  
> > [https://github.com/deech/ATSPresentation/blob/master/filter\_list.dats#L16](https://github.com/deech/ATSPresentation/blob/master/filter_list.dats#L16),  
> > I got this constraint error:  
> >   
> > “/home/deech/Downloads/ATS2-Postiats-0.2.1”/bin/patscc  
> > -DATS\_MEMALLOC\_LIBC -O2 -flto -o filter\_list filter\_list.dats || echo  
> > filter\_list “: ERROR!!!”  
> > /home/deech/ATS/ATSPresentation/filter\_list.dats: 432(line=16, offs=30)  
> > – 432(line=16, offs=30): error(3): unsolved constraint:  
> > C3NSTRprop(C3TKmain(); S2Eapp(S2Ecst(\>=);  
> > S2EVar(4410-\>S2Evar(k$7234$7235$7236(12754))), S2Eintinf(0)))  
> > typechecking has failed: there are some unsolved constraints: please  
> > inspect the above reported error message(s) for information.  
> > exit(ATS): uncaught exception:  
> > \_2home\_2hwxi\_2research\_2Postiats\_2git\_2src\_2pats\_error\_2esats\_\_FatalErrorExn(1025)  
> > filter\_list : ERROR!!!
> > 
> > It seems to be asking for proof that some number ( which I assume to be  
> > the length of the rest of the list ) is \>= 0 but I’m not sure why. Can  
> > anyone explain?
> > 
> > Thanks!  
> > -deech

---

<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:** [August 8, 2015, 1:46pm UTC](https://discourse.ats-lang.org/t/weird-lemma-in-ats-filter-function-b/102/7 "2015-08-08T13:46:18Z")

</div>

By the way, it is unnecessary to use fold@ to implement  
list\_vt\_filter given in the presentation as list\_vt\_filter only uses  
its first argument in a read-only fashion. The pattern  
@list\_vt\_cons(x, xs) is for gaining access to the pointers inside  
a linear list-node.On Saturday, August 8, 2015 at 1:27:24 AM UTC-4, Kiwamu Okabe wrote:

> Hi aditya,
> 
> On Sat, Aug 8, 2015 at 5:57 AM, aditya siram \<[adit...@gmail.com](mailto:adit...@gmail.com) \<javascript:\>\> wrote:
> 
> > I recently gave a talk on ATS  
> > \*[https://github.com/deech/ATSPresentation/blob/master/presentation.org](https://github.com/deech/ATSPresentation/blob/master/presentation.org))  
> > and
> 
> ## Thank’s for your great slide. Today, I understand “fold@” on your slide.
> 
> Kiwamu Okabe at METASEPI DESIGN

---

<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:** [August 8, 2015, 2:09am UTC](https://discourse.ats-lang.org/t/weird-lemma-in-ats-filter-function-b/102/8 "2015-08-08T02:09:49Z")

</div>

I added a tail-recursive version of list\_vt\_filter:

[https://github.com/githwxi/ATS-Postiats-test/blob/master/core/MISC/test06.datsOn](https://github.com/githwxi/ATS-Postiats-test/blob/master/core/MISC/test06.datsOn) Friday, August 7, 2015 at 9:08:31 PM UTC-4, gmhwxi wrote:

> I tidied up the code a bit. See:
> 
> [https://github.com/githwxi/ATS-Postiats-test/blob/master/core/MISC/test06.dats](https://github.com/githwxi/ATS-Postiats-test/blob/master/core/MISC/test06.dats)
> 
> If you change [k: int | k \<= n] to [k: nat | k \<= n], then the lemma is  
> not needed.  
> The need for the lemma is due to list\_vt\_cons requiring its second  
> argument to be  
> a list of non-negative length. Yes, every length is non-negative, but the  
> typechecker  
> of ATS does not know this fact.
> 
> The tail-call in the filter function is not eliminated. I will fix this  
> issue in the next release  
> of ATS. For now, if you want the tail-call to be eliminated, please use  
> the following coding  
> style:
> 
> extern fun list\_vt\_filter …  
> implement{a} list\_vt\_filter (xs, f) = …
> 
> On Friday, August 7, 2015 at 4:57:03 PM UTC-4, aditya siram wrote:
> 
> > Hi all,  
> > I recently gave a talk on ATS \*  
> > [https://github.com/deech/ATSPresentation/blob/master/presentation.org](https://github.com/deech/ATSPresentation/blob/master/presentation.org))  
> > and attempted to write a function that filtered a linear polymorphic list:  
> > [https://github.com/deech/ATSPresentation/blob/master/filter\_list.dats#L5](https://github.com/deech/ATSPresentation/blob/master/filter_list.dats#L5).
> > 
> > Without the line:  
> > [https://github.com/deech/ATSPresentation/blob/master/filter\_list.dats#L16](https://github.com/deech/ATSPresentation/blob/master/filter_list.dats#L16),  
> > I got this constraint error:  
> >   
> > “/home/deech/Downloads/ATS2-Postiats-0.2.1”/bin/patscc  
> > -DATS\_MEMALLOC\_LIBC -O2 -flto -o filter\_list filter\_list.dats || echo  
> > filter\_list “: ERROR!!!”  
> > /home/deech/ATS/ATSPresentation/filter\_list.dats: 432(line=16, offs=30)  
> > – 432(line=16, offs=30): error(3): unsolved constraint:  
> > C3NSTRprop(C3TKmain(); S2Eapp(S2Ecst(\>=);  
> > S2EVar(4410-\>S2Evar(k$7234$7235$7236(12754))), S2Eintinf(0)))  
> > typechecking has failed: there are some unsolved constraints: please  
> > inspect the above reported error message(s) for information.  
> > exit(ATS): uncaught exception:  
> > \_2home\_2hwxi\_2research\_2Postiats\_2git\_2src\_2pats\_error\_2esats\_\_FatalErrorExn(1025)  
> > filter\_list : ERROR!!!
> > 
> > It seems to be asking for proof that some number ( which I assume to be  
> > the length of the rest of the list ) is \>= 0 but I’m not sure why. Can  
> > anyone explain?
> > 
> > Thanks!  
> > -deech