Hi Hongwei,
On Wed, Jun 15, 2016 at 4:55 PM, Hongwei Xi <gmh...@gmail.com> wrote:
> chss is not a sort; it is a subset sort, which can not be
> used to index a type. Try:
>
> abstype chss(int)
>
> praxi lemma_chss{n:int} (!chss(n)): [0 <= n; n <= 7] void
I wrote following code:
```
#define chss_init 0
#define chss_ilock 7
absvtype chss(s:int)
extern praxi lemma_chss {n:int} (!chss(n)): [chss_init <= n; n <=
chss_ilock] void
fun foofunc (pss: !chss(10) | p: ptr): void = {
}
```
However it's type-checked...
How to avoid out of bound over the chss's int?
How to use `lemma_chss`?
Best regards,
--
Kiwamu Okabe at METASEPI DESIGN
--
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-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@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/CAEvX6dktUiGvAz40Qi_wDgoHazyYuSAKNMPXEUbS%3Dok7reDm%2BQ%40mail.gmail.com.
