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–17 of 1347
Welcome to the ats-lang-users group!
Mark all as read
Report group
0 selected
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
gmhwxi
,
Steinway Wu
4
7/4/17
Q&A
Declaring a static constant with an external name
I put up a PR for your consideration. https://github.com/githwxi/ATS-Postiats/pull/170 On Tuesday,
unread,
constraint
documentation
syntax
Q&A
Declaring a static constant with an external name
I put up a PR for your consideration. https://github.com/githwxi/ATS-Postiats/pull/170 On Tuesday,
7/4/17
gmhwxi
2
6/26/16
Q&A
patsolve_smt2
You can solve the above generated constraints using Z3. You can also use cvc4, but some non-linear
unread,
constraint
Q&A
patsolve_smt2
You can solve the above generated constraints using Z3. You can also use cvc4, but some non-linear
6/26/16
gmhwxi
6/23/16
Q&A
Support for solving constraints on reals
I have recently added support for generating constraints on reals in ATS. The generated constraints
unread,
constraint
Q&A
Support for solving constraints on reals
I have recently added support for generating constraints on reals in ATS. The generated constraints
6/23/16
Kiwamu Okabe
,
Hongwei Xi
30
7/10/16
Real-time OS system state captured by ATS language (and questions)
Great! Posted as a news piece at http://www.ats-lang.org/Community.html ---------- Forwarded message
unread,
constraint
syntax
type
Real-time OS system state captured by ATS language (and questions)
Great! Posted as a news piece at http://www.ats-lang.org/Community.html ---------- Forwarded message
7/10/16
gmhwxi
, …
Steinway Wu
11
7/17/16
Q&A
Embedding differential equations into types
I see. Thanks! On Saturday, July 16, 2016 at 11:58:44 PM UTC-4, gmhwxi wrote: In this case, the
unread,
constraint
Q&A
Embedding differential equations into types
I see. Thanks! On Saturday, July 16, 2016 at 11:58:44 PM UTC-4, gmhwxi wrote: In this case, the
7/17/16
Yannick Duchêne
,
Hongwei Xi
5
12/22/15
Q&A
Recursion inside well founded dataprops: any implicite termination metrics?
Le mardi 22 décembre 2015 22:14:34 UTC+1, gmhwxi a écrit : ATS is not a formal theorem-proving system
unread,
constraint
syntax
Q&A
Recursion inside well founded dataprops: any implicite termination metrics?
Le mardi 22 décembre 2015 22:14:34 UTC+1, gmhwxi a écrit : ATS is not a formal theorem-proving system
12/22/15
Yannick Duchêne
3
12/22/15
Q&A
Dataprop: indexes vs constraint parameters
Le mardi 22 décembre 2015 16:08:38 UTC+1, Yannick Duchêne a écrit : I personally will ban the style
unread,
constraint
example
tutorial
Q&A
Dataprop: indexes vs constraint parameters
Le mardi 22 décembre 2015 16:08:38 UTC+1, Yannick Duchêne a écrit : I personally will ban the style
12/22/15
Yannick Duchêne
,
gmhwxi
21
12/13/15
Q&A
Stadef and stacst questions: am I missing Skolen constants?
Le dimanche 13 décembre 2015 22:21:11 UTC+1, gmhwxi a écrit : From Q to P: prfn Q2P (pf: Q): P = let
unread,
constraint
proof
theorem-proving
Q&A
Stadef and stacst questions: am I missing Skolen constants?
Le dimanche 13 décembre 2015 22:21:11 UTC+1, gmhwxi a écrit : From Q to P: prfn Q2P (pf: Q): P = let
12/13/15
Yannick Duchêne
, …
gmhwxi
12
12/13/15
Q&A
Constraint solver: what can safely be assumed about its capacity?
Le lundi 14 décembre 2015 03:38:39 UTC+1, gmhwxi a écrit : I took a look at the implementation of
unread,
constraint
documentation
portability
Q&A
Constraint solver: what can safely be assumed about its capacity?
Le lundi 14 décembre 2015 03:38:39 UTC+1, gmhwxi a écrit : I took a look at the implementation of
12/13/15
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
gmhwxi
, …
john skaller
13
6/16/15
Q&A
Quantifed constraints
On 17/06/2015, at 7:26 AM, H Zhang wrote: > You might want to try Kodkod http://alloy.mit.edu/
unread,
constraint
proof
theorem-proving
Q&A
Quantifed constraints
On 17/06/2015, at 7:26 AM, H Zhang wrote: > You might want to try Kodkod http://alloy.mit.edu/
6/16/15
Yannick Duchêne
, …
gmhwxi
27
12/11/15
Q&A
Universal quantifier on function result: does it means what it looks to?
Le samedi 16 mai 2015 06:12:39 UTC+2, Artyom Shalkhakov a écrit : How about this one? absprop
unread,
constraint
Q&A
Universal quantifier on function result: does it means what it looks to?
Le samedi 16 mai 2015 06:12:39 UTC+2, Artyom Shalkhakov a écrit : How about this one? absprop
12/11/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
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
Hongwei Xi
2
3/30/14
Re: Unsolved constraint in factorial example
Here is a version that type-checks: fun fact{n:nat} ( x: int n ) : [r:nat] int r = ( if x > 0 then
unread,
constraint
Re: Unsolved constraint in factorial example
Here is a version that type-checks: fun fact{n:nat} ( x: int n ) : [r:nat] int r = ( if x > 0 then
3/30/14
Shahab Tasharrofi
,
gmhwxi
2
3/29/14
Q&A
Existential constraint solving
Basically, the issue here is to show the following type equality: NatLt(ds) = NatLt(ds) Currently,
unread,
constraint
Q&A
Existential constraint solving
Basically, the issue here is to show the following type equality: NatLt(ds) = NatLt(ds) Currently,
3/29/14