So, I think I understand somethings...
https://github.com/jats-ug/practice-ats/blob/d19b4a2739a332158a08d1deabe25d9eef71388a/mutual_record/main.dats
https://github.com/jats-ug/practice-ats/blob/d19b4a2739a332158a08d1deabe25d9eef71388a/mutual_struct/main.dats
Following define doesn't make sense.
```
vtypedef bar = @{ x= int, p= [l:addr] (foo@l | ptr(l)) }
vtypedef foo = $extype_struct"struct foo" of {
x = int,
p = [l:addr] (bar@l | ptr(l))
}
```
Following is good style:
```
vtypedef foo = @{ x= int, p= [l:addr] ptr(l) }
vtypedef bar = $extype_struct"struct bar" of {
x = int,
p = [l:addr] ptr(l)
}
```
Because, any function can't watch linear proof inside of vtypedef.
If we would like to specify the linear proof, we should dump the
vtypedef and add the proof as following:
```
fun print_foo' {l1,l2:addr} (pffoo: !(@{ x= int, p= ptr(l2) })@l1,
pfbar: !bar@l2 | p: ptr(l1)): void = {
val () = println! ("foo.x = ", p->x)
val () = println! ("bar.x = ", p->p->x)
}
```
Is it correct?
Best regards,
--
Kiwamu Okabe
--
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%3DV5O_fERVLpKpT_MC7s8gNTQDuPxffhe8w896H94j%2B%2Bg%40mail.gmail.com.
