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

Lean: issue429 test fails #1156

Open
protoben opened this issue Mar 11, 2025 · 1 comment
Open

Lean: issue429 test fails #1156

protoben opened this issue Mar 11, 2025 · 1 comment
Labels
Lean Issues with Sail to Lean translation

Comments

@protoben
Copy link
Collaborator

The issue429 Lean test fails with the following type error:

error: ././././Out.lean:102:31: application type mismatch
  get_value32 x
argument
  x
has type
  two_bitvectors k_n : Type
but is expected to have type
  two_bitvectors 32 : Type
@protoben protoben added the Lean Issues with Sail to Lean translation label Mar 11, 2025
@Alasdair
Copy link
Collaborator

For reference, is a regression test for this issue: #429

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Lean Issues with Sail to Lean translation
Projects
None yet
Development

No branches or pull requests

2 participants