# Hax Lean library
This folder contains the Lean library necessary to use hax-extracted rust code
in Lean. It is organized as follows:
- `Lib.lean` : main prelude definitions (integer types, arrays, errors, etc)
- `BitVec.lean` : additional lemmas and tactics to handle bitvectors