We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent e3a8082 commit 33ce662Copy full SHA for 33ce662
Batteries/Data/BitVec/Lemmas.lean
@@ -23,7 +23,7 @@ namespace BitVec
23
rfl
24
25
@[simp] theorem toFin_ofFnLEAux (m : Nat) (f : Fin n → Bool) :
26
- (ofFnLEAux m f).toFin = Fin.ofNat' (2 ^ m) (Nat.ofBits f) := by
+ (ofFnLEAux m f).toFin = Fin.ofNat (2 ^ m) (Nat.ofBits f) := by
27
ext; simp
28
29
@[simp] theorem toNat_ofFnLE (f : Fin n → Bool) : (ofFnLE f).toNat = Nat.ofBits f := by
0 commit comments