temporary fix, revert after merging

kmill · kmill · commit f11f67fd2fc8 · 2025-02-17T14:30:33.000-08:00
diff --git a/src/Init/Data/UInt/Lemmas.lean b/src/Init/Data/UInt/Lemmas.lean
@@ -11,6 +11,8 @@ import Init.Data.BitVec.Bitblast
 
 open Lean in
 set_option hygiene false in
+-- TODO(kmill): needed this for bootstrapping issue, remove option
+set_option interpreter.prefer_native false in
 macro "declare_uint_theorems" typeName:ident bits:term:arg : command => do
   let mut cmds ← Syntax.getArgs <$> `(
   namespace $typeName
