foofunc cannot be used as long as there is no way to produce a value of the type chss(10).
You can form the type chss(10), but you should allow a value of this type to be formed. For instance, list(string, ~1) is a valid type but there is no value of such a type. On Wed, Jun 15, 2016 at 4:13 AM, Kiwamu Okabe <[email protected]> wrote: > Hi Hongwei, > > On Wed, Jun 15, 2016 at 4:55 PM, Hongwei Xi <[email protected]> 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 [email protected]. > To post to this group, send email to [email protected]. > 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 > . > -- 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 [email protected]. To post to this group, send email to [email protected]. 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/CAPPSPLr044bam5Kfu99a_bXoZK9aiYfZCDbSxLF%3DVUAt0QM7HA%40mail.gmail.com.
