On Sat, Sep 24, 2016 at 6:06 AM, gmhwxi <gmh...@gmail.com> wrote:
> I think we need to be able to translate function bodies.
Umm... I also think it's useful for real programming.
However, do you think it's worth while using following unsafe proof function?
```
extern praxi __create_view {to:view} ():<prf> to
extern praxi __consume_view {from:view} (pf: from):<prf> void
```
For me, it's not trivial that translating C into ATS correctly use
dependent/linear types without such unsafe things... Of course, after
automatically translating, we can modify the generated code into a
style correctly using proof.
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 ats-lang-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
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/CAEvX6dn3hutnL9wYp%2BHYNDk3%2BQnPx2haFxkkE22zXaKDdT5q4g%40mail.gmail.com.
