# The thread of the errors in the docs

**URL:** <https://discourse.ats-lang.org/t/the-thread-of-the-errors-in-the-docs/17>\
**Category:** Google Group\
**Created:** [January 28, 2015, 5:49pm UTC](https://discourse.ats-lang.org/t/the-thread-of-the-errors-in-the-docs/17 "2015-01-28T17:49:32Z")\
**Posts on this page:** 20\
**Page:** 1

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [January 28, 2015, 5:49pm UTC](https://discourse.ats-lang.org/t/the-thread-of-the-errors-in-the-docs/17/1 "2015-01-28T17:49:32Z")

</div>

I don’t remember of any already existing one, so I’m opening this thread  
where to report any errors in the docs, instead of opening a new thread for  
each possible eventual errors (saying that, I don’t want to mean there are  
many).

My first case.

In [http://ats-lang.sourceforge.net/DOCUMENT/ATS2TUTORIAL/HTML/c309.html](http://ats-lang.sourceforge.net/DOCUMENT/ATS2TUTORIAL/HTML/c309.html) :

```
 val
 fact =
 fix f(x: int): int =>
   if x > 0 then x * fact(x-1) else 1
 (* end of [fact] *)

```

Sure it should be “f(x-1)” instead of “fact(x-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:** [May 22, 2015, 2:00pm UTC](https://discourse.ats-lang.org/t/the-thread-of-the-errors-in-the-docs/17/2 "2015-05-22T14:00:45Z")

</div>

This section has not been written yet. I will find some time to do it.On Thu, May 21, 2015 at 5:50 PM, ‘Yannick Duchêne’ via ats-lang-users \< [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com)\> wrote:

> I’m a bit unsure with this one, rather a doubt.
> 
> In  
> [http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x3658.html](http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x3658.html)  
> , the wording suggest something is to come, but the page contains a single  
> sentence.
> 
> Le mercredi 28 janvier 2015 18:49:32 UTC+1, Yannick Duchêne a écrit :
> 
> > I don’t remember of any already existing one, so I’m opening this thread  
> > where to report any errors in the docs, instead of opening a new thread for  
> > each possible eventual errors (saying that, I don’t want to mean there are  
> > many).
> > 
> > […]
> 
> –  
> 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).  
> Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users).  
> To view this discussion on the web visit  
> [https://groups.google.com/d/msgid/ats-lang-users/4b1809f7-2099-4943-ae98-1c2064666d72%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/4b1809f7-2099-4943-ae98-1c2064666d72%40googlegroups.com)  
> [https://groups.google.com/d/msgid/ats-lang-users/4b1809f7-2099-4943-ae98-1c2064666d72%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/4b1809f7-2099-4943-ae98-1c2064666d72%40googlegroups.com?utm_medium=email&utm_source=footer)  
> .

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [February 7, 2015, 12:27pm UTC](https://discourse.ats-lang.org/t/the-thread-of-the-errors-in-the-docs/17/3 "2015-02-07T12:27:54Z")

</div>

A tiny thing, a typo here:  
[http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/c2843.html](http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/c2843.html)

“Within the ATS programming _langauge_ system” (should be “language”)Le mercredi 28 janvier 2015 18:49:32 UTC+1, Yannick Duchêne a écrit :

> I don’t remember of any already existing one, so I’m opening this thread  
> where to report any errors in the docs, instead of opening a new thread for  
> each possible eventual errors (saying that, I don’t want to mean there are  
> many).

---

<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:** [February 6, 2015, 5:26pm UTC](https://discourse.ats-lang.org/t/the-thread-of-the-errors-in-the-docs/17/4 "2015-02-06T17:26:34Z")

</div>

Thanks for pointing it out.

I have changed (diff / 2) into half(diff). The type assigned to integer  
division in ATS2  
is no longer strong enough for this example.On Fri, Feb 6, 2015 at 12:07 PM, ‘Yannick Duchêne’ via ats-lang-users \< [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com)\> wrote:

> In [http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x2528.html](http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x2528.html)  
> , about the second definition of the `isqrt` function, this sentence looks  
> strange to me: “The following code we obtain after proper modification does  
> pass typechecking”. Actually, it does not: both `patscc --typecheck` and  
> `patscc -tcats` tells about one unsolved constraint error and two unsolved  
> termination constraints errors.
> 
> Le mercredi 28 janvier 2015 18:49:32 UTC+1, Yannick Duchêne a écrit :
> 
> > I don’t remember of any already existing one, so I’m opening this thread  
> > where to report any errors in the docs, instead of opening a new thread for  
> > each possible eventual errors (saying that, I don’t want to mean there are  
> > many).
> > 
> > –  
> > 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).  
> > Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users).  
> > To view this discussion on the web visit  
> > [https://groups.google.com/d/msgid/ats-lang-users/94b73663-3d66-4a5d-9da5-3764d6bd1391%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/94b73663-3d66-4a5d-9da5-3764d6bd1391%40googlegroups.com)  
> > [https://groups.google.com/d/msgid/ats-lang-users/94b73663-3d66-4a5d-9da5-3764d6bd1391%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/94b73663-3d66-4a5d-9da5-3764d6bd1391%40googlegroups.com?utm_medium=email&utm_source=footer)  
> > .

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [February 7, 2015, 3:38pm UTC](https://discourse.ats-lang.org/t/the-thread-of-the-errors-in-the-docs/17/5 "2015-02-07T15:38:07Z")

</div>

> Fixed. Thanks!

Thanks too! 😛

I found another typo, more annoying this one, as it ends into a  
type‑checker error. In  
[http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x2905.html](http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x2905.html)  
“prfun mut\_istot {m,n:int} (): [p:int] MUL (m, n, p)” the name “mut\_istot”  
should be “mul\_istot” or else the proof function implementation which  
follows fails.

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [February 6, 2015, 5:07pm UTC](https://discourse.ats-lang.org/t/the-thread-of-the-errors-in-the-docs/17/6 "2015-02-06T17:07:31Z")

</div>

In [http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x2528.html](http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x2528.html) ,  
about the second definition of the `isqrt` function, this sentence looks  
strange to me: “The following code we obtain after proper modification does  
pass typechecking”. Actually, it does not: both `patscc --typecheck` and  
`patscc -tcats` tells about one unsolved constraint error and two unsolved  
termination constraints errors.Le mercredi 28 janvier 2015 18:49:32 UTC+1, Yannick Duchêne a écrit :

> I don’t remember of any already existing one, so I’m opening this thread  
> where to report any errors in the docs, instead of opening a new thread for  
> each possible eventual errors (saying that, I don’t want to mean there are  
> many).

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [May 20, 2015, 5:08am UTC](https://discourse.ats-lang.org/t/the-thread-of-the-errors-in-the-docs/17/7 "2015-05-20T05:08:02Z")

</div>

> I don’t remember of any already existing one, so I’m opening this thread  
> where to report any errors in the docs, instead of opening a new thread for  
> each possible eventual errors (saying that, I don’t want to mean there are  
> many).
> 
> […]

Unless I’ve missed something, I believe there is a repeated error in  
[http://ats-lang.sourceforge.net/DOCUMENT/ATS2TUTORIAL/HTML/HTMLTOC/c642.html](http://ats-lang.sourceforge.net/DOCUMENT/ATS2TUTORIAL/HTML/HTMLTOC/c642.html)  
: `n` is never decremented.

At least, adding a termination metric, without touching the function’s  
logic, makes ATS catch an error:  
fun fact  
{n: int} (n: int n): int = let  
fun loop {n: int} .. (n: int n, res: int): int =  
if n \> 0 then loop (n, n \* res) else res  
// end of [loop]  
in  
loop (n, 1)  
end // end of [fact]

This one is OK:  
fun fact  
{n: nat} (n: int n): int = let  
fun loop {n: nat} .. (n: int n, res: int): int =  
if n \> 0 then loop (n - 1, n \* res) else res  
// end of [loop]  
in  
loop (n, 1)  
end // end of [fact]

This seems to be the same with the two preceding functions.

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [May 14, 2015, 12:28pm UTC](https://discourse.ats-lang.org/t/the-thread-of-the-errors-in-the-docs/17/8 "2015-05-14T12:28:25Z")

</div>

Not an error, just a comment.

On the page  
[http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x2110.html](http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x2110.html)  
, the definition of `array_copy_from_list`, starts like this:

implement  
{a}(_tmp_)  
array\_copy\_from\_list  
(A, xs) = let

Looking only at the declaration part, how `a` is used is not visible. It is  
made visible later, making use of type inference:

```
  […] = let

```

//  
fun loop  
(  
p: ptr, xs: list0 (a)  
) : void =

Just wondered if ever this more easy to follow if `x: list0 (a)` was on the  
outer declaration, so that the relation would be more obvious. Like this:

implement  
{a}(_tmp_)  
array\_copy\_from\_list  
(A, xs: list0 (a)) = let

(provided I’ve not missed anything and I’m saying something wrong, as I’m  
not yet used to templates)Le mercredi 28 janvier 2015 18:49:32 UTC+1, Yannick Duchêne a écrit :

> I don’t remember of any already existing one, so I’m opening this thread  
> where to report any errors in the docs, instead of opening a new thread for  
> each possible eventual errors (saying that, I don’t want to mean there are  
> many).
> 
> My first case.  
> […]

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [February 10, 2015, 12:52pm UTC](https://discourse.ats-lang.org/t/the-thread-of-the-errors-in-the-docs/17/9 "2015-02-10T12:52:24Z")

</div>

In  
[http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x3166.html](http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x3166.html)  
, an invocation of `imul2` is wrong. In `val (pfmul | r1) = (i+1) imul2 r`  
should either be rewritten as `val (pfmul | r1) = (i+1) \imul2 r` or as  
`val (pfmul | r1) = imul2((i+1), r)`Le mercredi 28 janvier 2015 18:49:32 UTC+1, Yannick Duchêne a écrit :

> I don’t remember of any already existing one, so I’m opening this thread  
> where to report any errors in the docs, instead of opening a new thread for  
> each possible eventual errors (saying that, I don’t want to mean there are  
> many).

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [December 11, 2015, 8:02pm UTC](https://discourse.ats-lang.org/t/the-thread-of-the-errors-in-the-docs/17/10 "2015-12-11T20:02:17Z")

</div>

Not an error, rather what I believe may be misleading, if I understand  
correctly.

In “Example: Verified Fast Exponentiation”  
[http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x3252.html](http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x3252.html)

An `absprop` `MUL` is defined, then follows the declaration of a dynamic  
function `mul_elt_elt`, returning a proof of `MUL(x, y, xy)`.

This function has no body, and indeed, there is no way for a dynamic  
function to instantiate a `MUL`, as it’s an abstract proposition, thus, not  
defining any dynamic constructor which would be usable from the body of a  
dynamic function. This function declared with `fun`, behaves like a  
`praxi`, and I though this may be better to use `praxi`.

I just wondered what about systematically use `praxi` is these cases, as it  
underlines it’s axiomatic (and one should always be careful with axioms).

Or is there a reason for it to be declared with `fun` instead of `praxi`?  
Especially in the documentation, `praxi` would be better, isn’t it?

There are two others in “Linear Channels for Asynchronous IPC”  
[http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x4355.html](http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x4355.html)

`queue_isnil` declared with `fun`, returning a proof of `ISNIL(id, b)` and  
`ISNIL` is an `absprop`  
`queue_isful` declared with `fun`, returning a proof of `ISFUL(id, b)` and  
`ISFUL` is an `absprop` too.

Unless I’m wrong…Le mercredi 28 janvier 2015 18:49:32 UTC+1, Yannick Duchêne a écrit :

> I don’t remember of any already existing one, so I’m opening this thread  
> where to report any errors in the docs, instead of opening a new thread for  
> each possible eventual errors (saying that, I don’t want to mean there are  
> many).

---

<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:** [February 7, 2015, 4:01pm UTC](https://discourse.ats-lang.org/t/the-thread-of-the-errors-in-the-docs/17/11 "2015-02-07T16:01:13Z")

</div>

Fixed. Thanks!On Sat, Feb 7, 2015 at 10:38 AM, ‘Yannick Duchêne’ via ats-lang-users \< [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com)\> wrote:

> Le samedi 7 février 2015 15:41:00 UTC+1, gmhwxi a écrit :
> 
> > Fixed. Thanks!
> 
> Thanks too! 😛
> 
> I found another typo, more annoying this one, as it ends into a  
> type‑checker error. In  
> [http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x2905.html](http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x2905.html)  
> “prfun mut\_istot {m,n:int} (): [p:int] MUL (m, n, p)” the name “mut\_istot”  
> should be “mul\_istot” or else the proof function implementation which  
> follows fails.
> 
> –  
> 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).  
> Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users).  
> To view this discussion on the web visit  
> [https://groups.google.com/d/msgid/ats-lang-users/be35a807-b960-4dd3-8773-259a2f6ab988%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/be35a807-b960-4dd3-8773-259a2f6ab988%40googlegroups.com)  
> [https://groups.google.com/d/msgid/ats-lang-users/be35a807-b960-4dd3-8773-259a2f6ab988%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/be35a807-b960-4dd3-8773-259a2f6ab988%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:** [January 28, 2015, 7:03pm UTC](https://discourse.ats-lang.org/t/the-thread-of-the-errors-in-the-docs/17/12 "2015-01-28T19:03:03Z")

</div>

Thank you very much for opening this thread. It is a VERY good idea!On Wednesday, January 28, 2015 at 12:49:32 PM UTC-5, Yannick Duchêne wrote:

> I don’t remember of any already existing one, so I’m opening this thread  
> where to report any errors in the docs, instead of opening a new thread for  
> each possible eventual errors (saying that, I don’t want to mean there are  
> many).
> 
> My first case.
> 
> In [http://ats-lang.sourceforge.net/DOCUMENT/ATS2TUTORIAL/HTML/c309.html](http://ats-lang.sourceforge.net/DOCUMENT/ATS2TUTORIAL/HTML/c309.html) :
> 
> ```
> val
> fact =
> fix f(x: int): int =>
> if x > 0 then x * fact(x-1) else 1
> (* end of [fact] *)
> 
> ```
> 
> Sure it should be “f(x-1)” instead of “fact(x-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:** [December 12, 2015, 2:27am UTC](https://discourse.ats-lang.org/t/the-thread-of-the-errors-in-the-docs/17/13 "2015-12-12T02:27:05Z")

</div>

Originally (that is, in ATS1), there is checking to ensure that each  
declared  
prfun is implemented; if a prfun is not implemented, it needs to be  
declared as a praxi.  
In ATS2, this kind of checking is abandoned (as it seems too unwieldy in  
practice).  
So, there is little difference between prfun and praxi in ATS2.

Even for an abstract prop, using prfun still makes sense as the abstract  
prop can be  
implemented at some point. Say you have an abstract prop FOO. You can do

assume FOO = …

implement  
lemma\_for\_FOO (…) = …On Friday, December 11, 2015 at 3:02:17 PM UTC-5, Yannick Duchêne wrote:

> Not an error, rather what I believe may be misleading, if I understand  
> correctly.
> 
> In “Example: Verified Fast Exponentiation”
> 
> [http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x3252.html](http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x3252.html)
> 
> An `absprop` `MUL` is defined, then follows the declaration of a dynamic  
> function `mul_elt_elt`, returning a proof of `MUL(x, y, xy)`.
> 
> This function has no body, and indeed, there is no way for a dynamic  
> function to instantiate a `MUL`, as it’s an abstract proposition, thus, not  
> defining any dynamic constructor which would be usable from the body of a  
> dynamic function. This function declared with `fun`, behaves like a  
> `praxi`, and I though this may be better to use `praxi`.
> 
> I just wondered what about systematically use `praxi` is these cases, as  
> it underlines it’s axiomatic (and one should always be careful with axioms).
> 
> Or is there a reason for it to be declared with `fun` instead of `praxi`?  
> Especially in the documentation, `praxi` would be better, isn’t it?
> 
> There are two others in “Linear Channels for Asynchronous IPC”
> 
> [http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x4355.html](http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x4355.html)
> 
> `queue_isnil` declared with `fun`, returning a proof of `ISNIL(id, b)` and  
> `ISNIL` is an `absprop`  
> `queue_isful` declared with `fun`, returning a proof of `ISFUL(id, b)` and  
> `ISFUL` is an `absprop` too.
> 
> Unless I’m wrong…
> 
> Le mercredi 28 janvier 2015 18:49:32 UTC+1, Yannick Duchêne a écrit :
> 
> > I don’t remember of any already existing one, so I’m opening this thread  
> > where to report any errors in the docs, instead of opening a new thread for  
> > each possible eventual errors (saying that, I don’t want to mean there are  
> > many).

---

<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:** [May 14, 2015, 2:10pm UTC](https://discourse.ats-lang.org/t/the-thread-of-the-errors-in-the-docs/17/14 "2015-05-14T14:10:02Z")

</div>

This is fine. It just incurs a little bit extra typechecking.On Thursday, May 14, 2015 at 8:28:25 AM UTC-4, Yannick Duchêne wrote:

> Not an error, just a comment.
> 
> On the page  
> [http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x2110.html](http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x2110.html)  
> , the definition of `array_copy_from_list`, starts like this:
> 
> implement  
> {a}(_tmp_)  
> array\_copy\_from\_list  
> (A, xs) = let
> 
> Looking only at the declaration part, how `a` is used is not visible. It  
> is made visible later, making use of type inference:
> 
> ```
> […] = let
> 
> ```
> 
> //  
> fun loop  
> (  
> p: ptr, xs: list0 (a)  
> ) : void =
> 
> Just wondered if ever this more easy to follow if `x: list0 (a)` was on  
> the outer declaration, so that the relation would be more obvious. Like  
> this:
> 
> implement  
> {a}(_tmp_)  
> array\_copy\_from\_list  
> (A, xs: list0 (a)) = let
> 
> (provided I’ve not missed anything and I’m saying something wrong, as I’m  
> not yet used to templates)
> 
> Le mercredi 28 janvier 2015 18:49:32 UTC+1, Yannick Duchêne a écrit :
> 
> > I don’t remember of any already existing one, so I’m opening this thread  
> > where to report any errors in the docs, instead of opening a new thread for  
> > each possible eventual errors (saying that, I don’t want to mean there are  
> > many).
> > 
> > My first case.  
> > […]

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [February 10, 2015, 12:28pm UTC](https://discourse.ats-lang.org/t/the-thread-of-the-errors-in-the-docs/17/15 "2015-02-10T12:28:24Z")

</div>

> I don’t remember of any already existing one, so I’m opening this thread  
> where to report any errors in the docs, instead of opening a new thread for  
> each possible eventual errors (saying that, I don’t want to mean there are  
> many).

Not an error, more an enhancement.

In  
[http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x3121.html](http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x3121.html)  
, `imul2` is given this signature:

fun imul2{i,j:int}  
(i: int i, j: int j): [ij:int] (MUL(i, j, ij) | int ij)

After  
[http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x3140.html](http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x3140.html)  
, if I check this in a DATS file…

extern fn imul2  
{i,j:int}  
(i: int i, j: int j): [ij:int] (MUL(i, j, ij) | int ij)

dataprop FACT(int, int) =  
| FACTbas(0, 1)  
| {n:nat} {r1,r:int} FACTind(n, r) of (FACT(n-1, r1), MUL(n, r1, r))

fun ifact {n:nat} .. (n: int(n)):\<\> [r:int] (FACT(n, r) | int r) =  
if n = 0  
then (FACTbas() | 1)  
else  
let  
val (pf1 | r1) = ifact (n-1) // pf1: FACT(n-1, r1)  
val (pfmul | r) = imul2 (n, r1) // pfmul: FACT(n, r1, r)  
in (FACTind(pf1, pfmul) | r)  
end

… I get the error or warning “some disallowed effects may be incurred: 1”  
on line #15 (the one which invokes `imul2`).

After an another topic,  
[Redirecting to Google Groups](https://groups.google.com/forum/#!topic/ats-lang-users/MsaDGpgDp0I) , seems  
either `:<>` has to be removed from `ifact` or `:<>` added to `imul2`.

---

<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:** [February 10, 2015, 2:36pm UTC](https://discourse.ats-lang.org/t/the-thread-of-the-errors-in-the-docs/17/16 "2015-02-10T14:36:01Z")

</div>

Fixed. Thanks!On Tue, Feb 10, 2015 at 7:52 AM, ‘Yannick Duchêne’ via ats-lang-users \< [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com)\> wrote:

> In  
> [http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x3166.html](http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x3166.html)  
> , an invocation of `imul2` is wrong. In `val (pfmul | r1) = (i+1) imul2 r`  
> should either be rewritten as `val (pfmul | r1) = (i+1) \imul2 r` or as  
> `val (pfmul | r1) = imul2((i+1), r)`
> 
> Le mercredi 28 janvier 2015 18:49:32 UTC+1, Yannick Duchêne a écrit :
> 
> > I don’t remember of any already existing one, so I’m opening this thread  
> > where to report any errors in the docs, instead of opening a new thread for  
> > each possible eventual errors (saying that, I don’t want to mean there are  
> > many).
> 
> –  
> 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).  
> Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users).  
> To view this discussion on the web visit  
> [https://groups.google.com/d/msgid/ats-lang-users/1409a3c0-1abb-4b65-9942-bec61f64042d%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/1409a3c0-1abb-4b65-9942-bec61f64042d%40googlegroups.com)  
> [https://groups.google.com/d/msgid/ats-lang-users/1409a3c0-1abb-4b65-9942-bec61f64042d%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/1409a3c0-1abb-4b65-9942-bec61f64042d%40googlegroups.com?utm_medium=email&utm_source=footer)  
> .

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [May 21, 2015, 9:50pm UTC](https://discourse.ats-lang.org/t/the-thread-of-the-errors-in-the-docs/17/17 "2015-05-21T21:50:17Z")

</div>

I’m a bit unsure with this one, rather a doubt.

In  
[http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x3658.html](http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x3658.html)  
, the wording suggest something is to come, but the page contains a single  
sentence.Le mercredi 28 janvier 2015 18:49:32 UTC+1, Yannick Duchêne a écrit :

> I don’t remember of any already existing one, so I’m opening this thread  
> where to report any errors in the docs, instead of opening a new thread for  
> each possible eventual errors (saying that, I don’t want to mean there are  
> many).
> 
> […]

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [February 9, 2015, 11:38pm UTC](https://discourse.ats-lang.org/t/the-thread-of-the-errors-in-the-docs/17/18 "2015-02-09T23:38:39Z")

</div>

> I don’t remember of any already existing one, so I’m opening this thread  
> where to report any errors in the docs, instead of opening a new thread for  
> each possible eventual errors (saying that, I don’t want to mean there are  
> many).

In  
[http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x3076.html](http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x3076.html)  
, in the sentence “ATS with theorem-proving systems such as Isabel and Coq  
[…]”, Isabelle is misspelled: “le” is missing at the end.

---

<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:** [February 10, 2015, 12:40am UTC](https://discourse.ats-lang.org/t/the-thread-of-the-errors-in-the-docs/17/19 "2015-02-10T00:40:07Z")

</div>

Fixed. Thanks!

I have never used Isabelle 🙂

Tried Nuprl a bit and Coq a bit, too.

My theorem-proving experience largely came from  
using/implementing a system called TPS, which was  
a project led by Prof. Peter Andrews at CMU.On Monday, February 9, 2015 at 6:38:39 PM UTC-5, Yannick Duchêne wrote:

> Le mercredi 28 janvier 2015 18:49:32 UTC+1, Yannick Duchêne a écrit :
> 
> > I don’t remember of any already existing one, so I’m opening this thread  
> > where to report any errors in the docs, instead of opening a new thread for  
> > each possible eventual errors (saying that, I don’t want to mean there are  
> > many).
> 
> In  
> [http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x3076.html](http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x3076.html)  
> , in the sentence “ATS with theorem-proving systems such as Isabel and Coq  
> […]”, Isabelle is misspelled: “le” is missing at the end.

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [February 1, 2015, 12:17pm UTC](https://discourse.ats-lang.org/t/the-thread-of-the-errors-in-the-docs/17/20 "2015-02-01T12:17:23Z")

</div>

Unless I’ve missed something, there is one in  
[http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x794.html](http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x794.html)

It says “For instance, calling rtfind on the polynomial function lam x =\> x

- x - x + 110 returns 11”. But x² - x + 110 = 0 has no solution in ℝ.  
Testing the example returns the erroneous result 463410 on my 32 bits  
machine.Le mercredi 28 janvier 2015 18:49:32 UTC+1, Yannick Duchêne a écrit :

> I don’t remember of any already existing one, so I’m opening this thread  
> where to report any errors in the docs, instead of opening a new thread for  
> each possible eventual errors (saying that, I don’t want to mean there are  
> many).

[Next page](https://discourse.ats-lang.org/t/the-thread-of-the-errors-in-the-docs/17.md?page=2)