Son HO
Son HO
Yes, it is probably a distinct issue... But I will clause this only once all the snippets above get accepted by the translation.
I investigated the issue: it stems from the fact that the implementation does not properly handle joins of *loan* values. It is a known issue (the same problem appears in...
https://github.com/AeneasVerif/aeneas/pull/600 solves all the issues but the very first example, because the loop fixed point is not precise enough yet to notice that it is possible to retrieve access to...
For now I don't see situations where a user seriously doesn't want additional typeclasses, so I suggest we implement this. The real questions is: which typeclasses do we want? Also,...
Thanks for the issue! I've actually been thinking about this for a while. What I have in mind so far is that we should keep some meta information in the...
This looks super fun, that's a great idea 😆
> Can you point to the ICFP tutorial? I intend to create a repo with only the tutorial, and I'm still modifying it (see the last PR for instance), but...
> @sonmarcho I think this is almost ready, there might be still some vague TODOs, but it feels feature-complete, I will take it for a walk and try to come...
This is great, thanks!! I will review and merge asap.
I think this is a great idea! You don't have to do this for the whole library, but it would be good to document this somewhere, perhaps in the README...