chore: remove @[inline] from BitVec.cast

2026-03-26 23:04:07 +00:00 · 2024-03-21 14:50:12 +11:00
1 changed files with 1 additions and 1 deletions
--- a/src/Init/Data/BitVec/Basic.lean
+++ b/src/Init/Data/BitVec/Basic.lean
@@ -371,7 +371,7 @@ end relations
 section cast

 /-- `cast eq i` embeds `i` into an equal `BitVec` type. -/
-@[inline] def cast (eq : n = m) (i : BitVec n) : BitVec m := .ofNatLt i.toNat (eq ▸ i.isLt)
+def cast (eq : n = m) (i : BitVec n) : BitVec m := .ofNatLt i.toNat (eq ▸ i.isLt)

@[simp] theorem cast_ofNat {n m : Nat} (h : n = m) (x : Nat) :
    cast h (BitVec.ofNat n x) = BitVec.ofNat m x := by