Hi,
I recently came across glot.io, an online service that lets you run and
share snippets. It is open source, so I took the opportunity to add support
for our ATS programming language. They use docker image to run ATS code,
and the image I provide contains not only ATS, but also erlang/elixir/z3
and make. You have all the freedom to play with a lot of fun stuff in that
setting. What’s also cool is they provide the ability to embed the snippets
as a nice little widget/iframe, while keeping your files editable and
runnable!
I posted a proof for the admissibility of cut in intuitionistic logic here
https://glot.io/snippets/eegppgnisi, and you can actually run it and check
the proof using ATS/z3.
Some links:
that is very cool. nice work / congrats to everybody involved.
Bravo!On Sat, May 7, 2016 at 2:18 PM, Steinway Wu stein...@gmail.com wrote:
Hi,
I recently came across glot.io, an online service that lets you run and
share snippets. It is open source, so I took the opportunity to add support
for our ATS programming language. They use docker image to run ATS code,
and the image I provide contains not only ATS, but also erlang/elixir/z3
and make. You have all the freedom to play with a lot of fun stuff in that
setting. What’s also cool is they provide the ability to embed the snippets
as a nice little widget/iframe, while keeping your files editable and
runnable!
I posted a proof for the admissibility of cut in intuitionistic logic here
Admissibility of Cut for Intuitionistic Logic - ATS Snippet - glot.io, and you can actually run it and
check the proof using ATS/z3.
Some links:
–
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.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/ed7a507d-91e6-4647-b51c-f180969af73a%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/ed7a507d-91e6-4647-b51c-f180969af73a%40googlegroups.com?utm_medium=email&utm_source=footer
.
Sure, it is merged. It will be published in the next deployment.On Monday, May 9, 2016 at 9:57:03 AM UTC-4, gmhwxi wrote:
It is here:
https://github.com/githwxi/ATS-Postiats/blob/master/doc/PROJECT/MEDIUM/ats2langweb/theLogo/theLogo.png
On Mon, May 9, 2016 at 9:52 AM, Steinway Wu <stei...@gmail.com <javascript:>> wrote:
Sure, but where can I find the source file for the logo?
On Saturday, May 7, 2016 at 5:28:38 PM UTC-4, gmhwxi wrote:
Could you also make ATS logo shown in the entry for ATS?
On Saturday, May 7, 2016 at 2:18:45 PM UTC-4, Steinway Wu wrote:
Hi,
I recently came across glot.io, an online service that lets you run
and share snippets. It is open source, so I took the opportunity to add
support for our ATS programming language. They use docker image to run ATS
code, and the image I provide contains not only ATS, but also
erlang/elixir/z3 and make. You have all the freedom to play with a lot of
fun stuff in that setting. What’s also cool is they provide the ability to
embed the snippets as a nice little widget/iframe, while keeping your files
editable and runnable!
I posted a proof for the admissibility of cut in intuitionistic logic
here Admissibility of Cut for Intuitionistic Logic - ATS Snippet - glot.io, and you can actually run it
and check the proof using ATS/z3.
Some links:
–
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 <javascript:>.
To post to this group, send email to ats-l...@googlegroups.com
<javascript:>.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/16047368-20e9-4e94-9a68-5846e16443c2%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/16047368-20e9-4e94-9a68-5846e16443c2%40googlegroups.com?utm_medium=email&utm_source=footer
.
It is here:
https://github.com/githwxi/ATS-Postiats/blob/master/doc/PROJECT/MEDIUM/ats2langweb/theLogo/theLogo.pngOn Mon, May 9, 2016 at 9:52 AM, Steinway Wu stein...@gmail.com wrote:
Sure, but where can I find the source file for the logo?
On Saturday, May 7, 2016 at 5:28:38 PM UTC-4, gmhwxi wrote:
Could you also make ATS logo shown in the entry for ATS?
On Saturday, May 7, 2016 at 2:18:45 PM UTC-4, Steinway Wu wrote:
Hi,
I recently came across glot.io, an online service that lets you run and
share snippets. It is open source, so I took the opportunity to add support
for our ATS programming language. They use docker image to run ATS code,
and the image I provide contains not only ATS, but also erlang/elixir/z3
and make. You have all the freedom to play with a lot of fun stuff in that
setting. What’s also cool is they provide the ability to embed the snippets
as a nice little widget/iframe, while keeping your files editable and
runnable!
I posted a proof for the admissibility of cut in intuitionistic logic
here Admissibility of Cut for Intuitionistic Logic - ATS Snippet - glot.io, and you can actually run it
and check the proof using ATS/z3.
Some links:
–
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.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/16047368-20e9-4e94-9a68-5846e16443c2%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/16047368-20e9-4e94-9a68-5846e16443c2%40googlegroups.com?utm_medium=email&utm_source=footer
.
Could you also make ATS logo shown in the entry for ATS?On Saturday, May 7, 2016 at 2:18:45 PM UTC-4, Steinway Wu wrote:
Hi,
I recently came across glot.io, an online service that lets you run and
share snippets. It is open source, so I took the opportunity to add support
for our ATS programming language. They use docker image to run ATS code,
and the image I provide contains not only ATS, but also erlang/elixir/z3
and make. You have all the freedom to play with a lot of fun stuff in that
setting. What’s also cool is they provide the ability to embed the snippets
as a nice little widget/iframe, while keeping your files editable and
runnable!
I posted a proof for the admissibility of cut in intuitionistic logic here
Admissibility of Cut for Intuitionistic Logic - ATS Snippet - glot.io, and you can actually run it and
check the proof using ATS/z3.
Some links:
Here is my trial:
https://glot.io/snippets/eei9lei9w1On Saturday, May 7, 2016 at 3:27:52 PM UTC-4, gmhwxi wrote:
Bravo!
On Sat, May 7, 2016 at 2:18 PM, Steinway Wu wrote:
Hi,
I recently came across glot.io, an online service that lets you run and
share snippets. It is open source, so I took the opportunity to add support
for our ATS programming language. They use docker image to run ATS code,
and the image I provide contains not only ATS, but also erlang/elixir/z3
and make. You have all the freedom to play with a lot of fun stuff in that
setting. What’s also cool is they provide the ability to embed the snippets
as a nice little widget/iframe, while keeping your files editable and
runnable!
I posted a proof for the admissibility of cut in intuitionistic logic
here Admissibility of Cut for Intuitionistic Logic - ATS Snippet - glot.io, and you can actually run it
and check the proof using ATS/z3.
Some links:
–
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.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/ed7a507d-91e6-4647-b51c-f180969af73a%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/ed7a507d-91e6-4647-b51c-f180969af73a%40googlegroups.com?utm_medium=email&utm_source=footer
.
This is so awesome! Thank you!
OK, here’s my attempt:
The one-hole contexts remind of the dataviews used in old AVL tree and RB
tree implementations (from ATS1 libats/ngc) that were used to reconstruct
the trees after rebalancing.On Sunday, May 8, 2016 at 12:18:45 AM UTC+6, Steinway Wu wrote:
Hi,
I recently came across glot.io, an online service that lets you run and
share snippets. It is open source, so I took the opportunity to add support
for our ATS programming language. They use docker image to run ATS code,
and the image I provide contains not only ATS, but also erlang/elixir/z3
and make. You have all the freedom to play with a lot of fun stuff in that
setting. What’s also cool is they provide the ability to embed the snippets
as a nice little widget/iframe, while keeping your files editable and
runnable!
I posted a proof for the admissibility of cut in intuitionistic logic here
Admissibility of Cut for Intuitionistic Logic - ATS Snippet - glot.io, and you can actually run it and
check the proof using ATS/z3.
Some links:
Sure, but where can I find the source file for the logo?On Saturday, May 7, 2016 at 5:28:38 PM UTC-4, gmhwxi wrote:
Could you also make ATS logo shown in the entry for ATS?
On Saturday, May 7, 2016 at 2:18:45 PM UTC-4, Steinway Wu wrote:
Hi,
I recently came across glot.io, an online service that lets you run and
share snippets. It is open source, so I took the opportunity to add support
for our ATS programming language. They use docker image to run ATS code,
and the image I provide contains not only ATS, but also erlang/elixir/z3
and make. You have all the freedom to play with a lot of fun stuff in that
setting. What’s also cool is they provide the ability to embed the snippets
as a nice little widget/iframe, while keeping your files editable and
runnable!
I posted a proof for the admissibility of cut in intuitionistic logic
here Admissibility of Cut for Intuitionistic Logic - ATS Snippet - glot.io, and you can actually run it
and check the proof using ATS/z3.
Some links:
