hax_lib::fstar::options!
: accept interface
/both
/impl
#896
Labels
hax_lib::fstar::options!
: accept interface
/both
/impl
#896
hax_lib::fstar::options!
is less expressive thanhax_lib::fstar::before!
orhax_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.
The text was updated successfully, but these errors were encountered: