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

self in requires clause gets renamed to self__ #1224

Open
karthikbhargavan opened this issue Jan 12, 2025 · 0 comments
Open

self in requires clause gets renamed to self__ #1224

karthikbhargavan opened this issue Jan 12, 2025 · 0 comments
Labels
backend Issue in one of the backends (i.e. F*, Coq, EC...) f* F* backend

Comments

@karthikbhargavan
Copy link
Contributor

When adding pre- and post-conditions to an impl block, I found a situation where references to self in the annotations result in malformed F*.

struct S(pub  u8);

#[hax_lib::attributes]
impl S {
    #[hax_lib::requires(self.0 == 0)]
    fn f(&self) {}
}

Open this code snippet in the playground

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
backend Issue in one of the backends (i.e. F*, Coq, EC...) f* F* backend
Projects
None yet
Development

No branches or pull requests

2 participants