Groups
Sign in
Groups
ats-lang-users
Conversations
Labels
API
ATS3
AVR
Clojure
Erlang
IDE
JVM
JavaScript
PHP
Perl
Python
Scheme
arduino
atsccomp
build
call-by-reference
call-by-value
closure
constraint
contribute
datatype
dependent-type
documentation
effect
emacs
example
general
high-order
install
library
license
linear-closure
linear-type
macro
package
polymorphism
portability
proof
refinement
session
stack-allocation
stream
syntax
tail-recursion
template
termination
theorem-proving
tutorial
type
type-error
About
Send feedback
Help
ats-lang-users
Contact owners and managers
1–15 of 1347
Welcome to the ats-lang-users group!
Mark all as read
Report group
0 selected
Yannick Duchêne
3/22/19
Q&A
Dependant types vs operational semantic
These past few days, I though it would be useful I plan to have some experiment with logic, in an
unread,
dependent-type
Q&A
Dependant types vs operational semantic
These past few days, I though it would be useful I plan to have some experiment with logic, in an
3/22/19
Bruno Zimmermann
,
Hongwei Xi
4
8/4/18
Q&A
How can I create a dependent size_t literal?
I myself usually just do: val zero = $UN.cast{size_t}(0) It may look a bit uglier but it is really
unread,
constraint
dependent-type
Q&A
How can I create a dependent size_t literal?
I myself usually just do: val zero = $UN.cast{size_t}(0) It may look a bit uglier but it is really
8/4/18
Max Hayden Chiz
,
gmhwxi
16
1/13/18
Q&A
How to do type-safe printf and GADT in ATS?
On Saturday, January 13, 2018 at 1:19:54 PM UTC-6, gmhwxi wrote: Since PrintfType can't be an ATS
unread,
dependent-type
example
Q&A
How to do type-safe printf and GADT in ATS?
On Saturday, January 13, 2018 at 1:19:54 PM UTC-6, gmhwxi wrote: Since PrintfType can't be an ATS
1/13/18
August Alm
, …
Artyom Shalkhakov
3
2/20/17
Q&A
Typechecking error involving Either datatype
Hi August, You could use this tool: https://ashalkhakov.github.io/pats-ef/ to turn the error message
unread,
dependent-type
type-error
Q&A
Typechecking error involving Either datatype
Hi August, You could use this tool: https://ashalkhakov.github.io/pats-ef/ to turn the error message
2/20/17
gmhwxi
, …
anonymous anonymous
11
2/11/16
Q&A
Imperative vs. functional vs. linear functional
I am glad you think that way. I also hope you have ATS in your preferences. On Wednesday, February 10
unread,
dependent-type
example
linear-type
Q&A
Imperative vs. functional vs. linear functional
I am glad you think that way. I also hope you have ATS in your preferences. On Wednesday, February 10
2/11/16
Shea Levy
,
Hongwei Xi
4
11/30/15
Q&A
Extracting the existentially-bound variables of an existentially quantified type?
Implementing such a function is more involved. See: https://groups.google.com/forum/#!searchin/ats-
unread,
constraint
dependent-type
Q&A
Extracting the existentially-bound variables of an existentially quantified type?
Implementing such a function is more involved. See: https://groups.google.com/forum/#!searchin/ats-
11/30/15
Yannick Duchêne
,
Hongwei Xi
12
5/14/15
Q&A
Indexed-type vs dependent-type
>>A variable of a default sort, Professor? A variable of a sort that can only be determined
unread,
dependent-type
type
Q&A
Indexed-type vs dependent-type
>>A variable of a default sort, Professor? A variable of a sort that can only be determined
5/14/15
Brandon Barker
,
Hongwei Xi
4
2/2/15
Q&A
modulo in constraints
The type for my_mod2 does not look right. On Mon, Feb 2, 2015 at 9:39 PM, Brandon Barker <brandon.
unread,
constraint
dependent-type
proof
Q&A
modulo in constraints
The type for my_mod2 does not look right. On Mon, Feb 2, 2015 at 9:39 PM, Brandon Barker <brandon.
2/2/15
gmhwxi
3
8/2/14
Q&A
ATS for MCU programming
... and accurate as well. On Saturday, August 2, 2014 12:59:16 PM UTC-4, gmhwxi wrote: Slide no. 12
unread,
dependent-type
linear-type
Q&A
ATS for MCU programming
... and accurate as well. On Saturday, August 2, 2014 12:59:16 PM UTC-4, gmhwxi wrote: Slide no. 12
8/2/14
Brandon Barker
,
gmhwxi
3
5/19/14
Q&A
cast a dependent type
I see ... sorta. I should read more about the solver. Brandon Barker brandon...@gmail.com On Mon,
unread,
dependent-type
Q&A
cast a dependent type
I see ... sorta. I should read more about the solver. Brandon Barker brandon...@gmail.com On Mon,
5/19/14
Brandon Barker
,
gmhwxi
17
5/15/14
Q&A
static integer multiplication
I am happy for you to do so - I have just been doing this for fun and learning, and I'm sure I
unread,
constraint
dependent-type
Q&A
static integer multiplication
I am happy for you to do so - I have just been doing this for fun and learning, and I'm sure I
5/15/14
gmhwxi
,
Artyom Shalkhakov
3
2/18/14
Q&A
Implementing strlen safely
Hi Artyom, str.tail expands to string_tail(str): fun string_tail {n:pos} (string(n)): string(n-1)
unread,
dependent-type
tail-recursion
Q&A
Implementing strlen safely
Hi Artyom, str.tail expands to string_tail(str): fun string_tail {n:pos} (string(n)): string(n-1)
2/18/14
Brandon Barker
,
gmhwxi
2
1/27/14
Q&A
the syntactic entity [s0qua] is needed
i<n changes to i < n. On Monday, January 27, 2014 6:33:27 PM UTC-5, Brandon Barker wrote:
unread,
dependent-type
Q&A
the syntactic entity [s0qua] is needed
i<n changes to i < n. On Monday, January 27, 2014 6:33:27 PM UTC-5, Brandon Barker wrote:
1/27/14
Brandon Barker
,
gmhwxi
5
1/24/14
Q&A
the static term is overly applied.
Here is my guess: abstype varname = string fun newmodel{nv:int} ( env: env, model: &model, mname:
unread,
dependent-type
Q&A
the static term is overly applied.
Here is my guess: abstype varname = string fun newmodel{nv:int} ( env: env, model: &model, mname:
1/24/14
Brandon Barker
,
gmhwxi
3
2/17/13
Q&A
Getting familiar with dependent types. (This is not a question, but a tutorial).
Yes, 'char' is a predicative sort. It is not used often so far. Most of the time, one just
unread,
dependent-type
documentation
Q&A
Getting familiar with dependent types. (This is not a question, but a tutorial).
Yes, 'char' is a predicative sort. It is not used often so far. Most of the time, one just
2/17/13