hacspec
`hax_lib::fstar::options!`: accept `interface`/`both`/`impl`
hax_lib::fstar::options! is less expressive than hax_lib::fstar::before! or hax_lib::fstar::after!. Those two accept an optional argument to specify where the annotation should go.
We need that on options (and friends) as well.
This is particularly useful for options on impl blocks, that (currently) only appears in interfaces (when interfaces are on). @karthikbhargavan had that problem with impls and zr3limit. Additionally we could also make the default smarter for impl blocks.
This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.
![github-actions[bot] avatar](https://avatars.githubusercontent.com/in/15368?v=4 "Published by a pub.dev verified publisher"){kind=small}
This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.
This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.
This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.
