Dear Hongwei, On Sun, Nov 11, 2018 at 11:33 PM Hongwei Xi <[email protected]> wrote: > >>A. I also believe we should replace `||` with + (badd). Is this correct? > > Yes, using '+' for '||' is correct.
Thanks. Clear for me. > >>B. How to write `not` in dependent type? > >>C. How to find such replacement between macro `&&` and `*`? > > Many boolean functions of dependent types > are declared in the following file: > > https://github.com/ats-lang/ats-lang.github.io/blob/master/ATS-Postiats/prelude/SATS/bool.sats ``` macdef || (b1, b2) = (if ,(b1) then true else ,(b2)): bool macdef && (b1, b2) = (if ,(b1) then ,(b2) else false): bool fun neg_bool0 (b: bool):<> bool = "mac#%" // overload ~ with neg_bool0 of 0 overload not with neg_bool0 of 0 fun add_bool0_bool0 (b1: bool, b2: bool):<> bool = "mac#%" fun mul_bool0_bool0 (b1: bool, b2: bool):<> bool = "mac#%" // overload + with add_bool0_bool0 of 0 overload * with mul_bool0_bool0 of 0 ``` Does it mean the operators introduced with `macdef` don't provide dependent type, ones introduced with `overload` provide dependent type? Also I panic on the operators with `overload`, which are just mapped to dynamic function. You said: > Replacing '&&' with * (bmul) should work, though. Where is the relationship between operator `*` and function `bmul`? > In practice, it is usually not about 'finding' the function you need; > instead, you can always declare > it on your own. I think above comment doesn't make sense... I would like to use dependent types, which is well defined at prelude or base library. Because it makes manner of code, which is more human readable. Why do I declare my own operator for dependent type? 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%3DBp-Ntd_FACF90SucYup%2Boxpki5M%2BEufX1MmhPe%3D%3D%2BGg%40mail.gmail.com.
