>>Where is the relationship between operator `*` and function `bmul`?
I misremembered. 'bmul' should be 'mul_bool1_bool1'. On Sun, Nov 11, 2018 at 9:45 PM Kiwamu Okabe <[email protected]> wrote: > 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 > . > -- 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/CAPPSPLr%3DVUUhZUxiqpKHSAr0Hpha0LvD3FQZD-4ZGLTJca3n7Q%40mail.gmail.com.
