Hi Hongwei, sorry for my waywardness. On Sun, Jun 19, 2016 at 12:38 AM, gmhwxi <[email protected]> wrote: > What you need can be captured in ATS as follows: > > (* ****** ****** *) > // > dataprop > chss_p(int) = {s:int | s <= 7} CHSS(s) of () > // > (* ****** ****** *) > // > abst@ype event_source_t > // > extern > fun > chEvtObjectInit > {s:int} > (!chss(s), chss_p(s) | cPtr0(event_source_t)): void = "mac#"
I feed the using chss_p on every function is messy, because every function needs two proof value... Is it able to define `absvtype chss(s:int)` as private definition? Please imagine following: ``` absvtype chss(s:int) vtypedef chss_sinit = chss(chss_init) vtypedef chss_any = [s:int | chss_init <= s; s <= chss_ilock] chss(s) vtypedef chss_iclass = [s:int | s == chss_slock || s == chss_ilock] chss(s) ``` I think threre are no miss calling like `chss(10)` in application code, if application programmer is permitted to access `chss_sinit` / `chss_any` / `chss_iclass` and prohibited to access `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/CAEvX6d%3D-v%3DO8YNpRCzz6pSG7ouTthQzbG9479hotsfoG35F-ZQ%40mail.gmail.com.
