diff --git a/Ix/Aiur/Goldilocks.lean b/Ix/Aiur/Goldilocks.lean
index d997400e..97ad74f7 100644
--- a/Ix/Aiur/Goldilocks.lean
+++ b/Ix/Aiur/Goldilocks.lean
@@ -7,7 +7,7 @@ namespace Aiur
 abbrev gSize : UInt64 := 1 - 2 ^ 32
 abbrev G := { u : UInt64 // u < gSize }
 
-@[inline] def G.ofNat (n : Nat) : G :=
+def G.ofNat (n : Nat) : G :=
   let n := n.toUInt64
   if h : n < gSize then ⟨n, h⟩
   else ⟨n % gSize, UInt64.mod_lt n (by decide)⟩