Yes, indeed, there are proof functions and proof values (as result of proof
functions) ; the word “proof” used alone is typically to mean proof
function (I was unclear).
Le samedi 23 mars 2019 22:35:51 UTC+1, gmhwxi a écrit :
>
> No, a proof is not a type. A proof is a total program (that is
Le mardi 7 août 2018 21:40:16 UTC+2, gmhwxi a écrit :
>
> >>Python surprisingly does not have direct support for arrays,
>
> Python is not famous for being effcient :)
>
I know, at least 40x worse than the equivalent in any imperative language.
I’m using it rather for its terse syntax (and
Le mardi 7 août 2018 10:04:58 UTC+2, Yannick Duchêne a écrit :
>
> […] It was not my matter, but may be for arrays with multiple dimension,
> using abstract types and external implementation may be an option, but I
> have never tried it.
>
Or rather interpret one-dimension array as the
Le mardi 7 août 2018 10:00:51 UTC+2, Yannick Duchêne a écrit :
>
> […]
> By the way, I wonder why `#include "share/atspre_staload.hats"` of the
> basics which are always loaded by default, because
> "share/atspre_staload.hats" seems often required.
>
Typo, sorry. I wanted to say “I wonder
Le mardi 7 août 2018 04:18:01 UTC+2, gmhwxi a écrit :
>
>
> @[int][3] is the type for a flat int array of size 3.
>
> Unfortunately, it is not fully supported at this point
> (it can only be assigned to a var). Please use @(int, int, int)
> instead.
>
Indeed, this works if there are only
Le mardi 7 août 2018 03:37:55 UTC+2, Julian Fondren a écrit :
>
> Incidentally, this works:
>
> #include "share/atspre_staload.hats"
>
> typedef row = @(int, int, int)
> val row1: row = (1, 2, 3)
> val row2: row = (4, 5, 6)
> var a = @[row](row1, row2)
> val a12 = a[1].2
>
> implement main0() =
I’m unsure if it’s something wrong with what I wrote (ex. may be it’s not
allowed) or with Postiats. The sample below type‑checks, but compilation
fails with an INTERROR message.
The sample:
typedef row = @[int][3]
val row1:row = @[int](1, 2, 3)
val row2:row = @[int](4,
Le samedi 4 août 2018 16:43:28 UTC+2, gmhwxi a écrit :
>
> Here is what I have in mind at this moment:
>
> ATS3 = ATS2 + meta-programming
>
> Type inference plays a big role to provide support for meta-programming.
>
That’s fine :)
--
You received this message because you are subscribed to
Le samedi 4 août 2018 16:38:00 UTC+2, gmhwxi a écrit :
>
> […]
> >>var h:t = lam@() => ()// <-- here
>
> 'var h:t' means that the size of 'h' is that of the size of 't'.
> It does NOT mean that only a value of the type 't' can be
> stored in 'h'.
>
Indeed, if I do what’s below, the function
Le vendredi 3 août 2018 22:18:48 UTC+2, Yannick Duchêne a écrit :
>
>
>
> Le vendredi 3 août 2018 22:17:24 UTC+2, Yannick Duchêne a écrit :
>>
>>
>> So `view@` peaks something?
>>
>>
> Oops, I wanted ti say “peek” instead of “peak”
>
Yes, I’m silly: view@ is subject to linear logic.
--
You
Le vendredi 3 août 2018 22:11:51 UTC+2, gmhwxi a écrit :
>
>
> It will be okay if you put 'p' back:
>
> // `g` evaluates `f` and then frees it.
> fn g(f: >> t?): int = let
> val r = f()
> val _ = cloptr_free($UN.castvwtp0(f))
> prval p
Here is sample, what’s important is in `g` marked `<-- here`:
staload UN = "prelude/SATS/unsafe.sats" // Prerequisite.
viewtypedef t = () - int // Prerequisite.
fn h(): t = let
val v = 1
in lam(): int => v end
// `g` evaluates `f` and then
Seems you are not the first one to face this issue
: https://github.com/gotk3/gotk3/issues/204
As Artyom said, it is POSIX related
: http://pubs.opengroup.org/onlinepubs/7908799/xsh/systypes.h.html
As an example, it appears in a struct for password entry
:
Le mercredi 1 août 2018 17:08:17 UTC+2, Artyom Shalkhakov a écrit :
>
> Hi Steinway,
>
> Thanks for your input!
>
> I think Yannick is very good at posing interesting questions. :-)
>
Documenting ATS2, deserves questionning :-D
--
You received this message because you are subscribed to the
If they are people using it, please, update it. I made an important change
since I mentioned it here. It's about a git command (among other smaller
things). I just remember to tell for some reason just now, I forget to tell
earlier. With my apologies …
Le jeudi 8 décembre 2016 15:49:49 UTC+1,
Le mardi 6 décembre 2016 17:47:16 UTC+1, gmhwxi a écrit :
>
> Yes. The issue should be fixed in the next release.
>
> The reason for the problem is that I myself rarely do 'make install' on my
> own computer when building ATS. So I forgot the need to change the version
> number in
>
Le mardi 6 décembre 2016 03:54:26 UTC+1, gmhwxi a écrit :
>
>
>
> If you could tell me how this happened, I would like to fix it. Thanks!
>
>
Oops, sorry, I should have tell more.
That's the subdirectory in lib, which is named `ats2-postiats-0.2.10` and
the wrapper scripts in `bin` which says
Le vendredi 2 décembre 2016 21:25:06 UTC+1, gmhwxi a écrit :
>
>
> I think I have fixed the issue. Please delete ATS2-contrib and
> try again.
>
Indeed, it works now (with Contrib from trunk).
Just that the ATS version looks like it is still 0.2.10 instead of 0.2.12.
Talking about Contrib, I
Installing the updated version using `C9-ATS2-install.sh`, I got this error:
cat: output/DATS/ML/list0_dats.php: Aucun fichier ou dossier de ce type
cat: output/DATS/ML/array0_dats.php: Aucun fichier ou dossier de ce type
« Aucun fichier ou dossier de ce type » means “No such file or
I guess substituting HTTP for HTTPS in the tutorial URL may solve the issue.
Le vendredi 5 août 2016 21:33:14 UTC+2, Steinway Wu a écrit :
>
> Sadly, there is a https related issue. I hope to fix it soon... for now,
> it works with Safari at least. I'm not particularly familiar of how to work
>
20 matches
Mail list logo
