New issue

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

#

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

Already on GitHub? # to your account

Jump to bottom

sail-to-lean: Properly deal with `int` valued bitvector lengths #956

Open

javra opened this issue Feb 4, 2025 · 0 comments

Labels

Lean

Collaborator

javra commented Feb 4, 2025

val nexp_mod_add : forall 'n. bitvector(2 ^ (- 'n)) -> bitvector(2 ^ (- 'n))

function nexp_mod_add x = {
  x
}

currently compiles to the invalid

/-- Type quantifiers: k_n : Int -/
def nexp_mod_add (x : (BitVec (2 ^ ((- k_n))))) : (BitVec (2 ^ ((- k_n)))) :=
  x

def initialize_registers (lit : Unit) : Unit :=
  ()

The text was updated successfully, but these errors were encountered:

javra added the Lean label

# for free to join this conversation on GitHub. Already have an account? # to comment