From ba51c0eef7f7ccd2be5afb6f16aa53766f1e406c Mon Sep 17 00:00:00 2001
From: Arthur Paulino <arthurleonardo.ap@gmail.com>
Date: Wed, 4 Mar 2026 16:50:35 -0300
Subject: [PATCH] chore: speed up Aiur elaboration

Inlining `G.ofNat` was making the Aiur elaboration program slow.
Removing the `@[inline]` tag from `G.ofNat` speeds up elaboration
by 2~3x.
---
 Ix/Aiur/Goldilocks.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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)⟩