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

F* cannot prove decidable equality with Hashmaps #1194

Open
maximebuyse opened this issue Dec 17, 2024 · 1 comment
Open

F* cannot prove decidable equality with Hashmaps #1194

maximebuyse opened this issue Dec 17, 2024 · 1 comment
Labels
f* F* backend libcore

Comments

@maximebuyse
Copy link
Contributor

struct s2(std::collections::HashMap<i32, i32>);

Open this code snippet in the playground

This seems to be a regression from #1166. F* fails on the HashMap argument with:

  - Failed to prove that the type
    'Playground.t_s2'
    supports decidable equality because of this argument.
  - Add either the 'noeq' or 'unopteq' qualifier
  - The SMT solver could not prove the query. Use --query_stats for more
    details.
  - See also Playground.fst(6,0-12,11)
@maximebuyse maximebuyse added f* F* backend libcore labels Dec 17, 2024
@maximebuyse
Copy link
Contributor Author

Should be fixed by 6701b54

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
f* F* backend libcore
Projects
None yet
Development

No branches or pull requests

1 participant