Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Error with hax_lib::fstar::before on impl method #1315

Open
maximebuyse opened this issue Feb 18, 2025 · 0 comments
Open

Error with hax_lib::fstar::before on impl method #1315

maximebuyse opened this issue Feb 18, 2025 · 0 comments
Labels
lib Lib-related issue (e.g. annotations lib)

Comments

@maximebuyse
Copy link
Contributor

struct Test();

impl Test {
    #[hax_lib::fstar::before(r"assume val v: i32")]
    fn f() {}
}

Open this code snippet in the playground
With the rust code above, when extracting to F*, I get the following error:

error: `const` items in this context need a name
 --> src/lib.rs:5:5
  |
5 |     #[hax_lib::fstar::before(r"assume val v: i32")]
  |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ `_` is not a valid name for this `const` item
  |
  = note: this error originates in the attribute macro `hax_lib::fstar::before` (in Nightly builds, run with -Z macro-backtrace for more info)

The generated F* corresponds to what is expected so that's not a big problem but it would be better if we didn't get the error.

@maximebuyse maximebuyse added the lib Lib-related issue (e.g. annotations lib) label Feb 18, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
lib Lib-related issue (e.g. annotations lib)
Projects
None yet
Development

No branches or pull requests

1 participant