From 46b126f4e0e86f14475bc310e150948434726dc7 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 8 Mar 2024 08:50:50 +0100
Subject: Update the handling of notations like #u32 or #isize

---
 backends/lean/Base/Arith/Scalar.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'backends/lean/Base/Arith')

diff --git a/backends/lean/Base/Arith/Scalar.lean b/backends/lean/Base/Arith/Scalar.lean
index 43fd2766..9441be86 100644
--- a/backends/lean/Base/Arith/Scalar.lean
+++ b/backends/lean/Base/Arith/Scalar.lean
@@ -74,7 +74,7 @@ example : U32.ofInt 1 ≤ U32.max := by
   scalar_tac
 
 example (x : Int) (h0 : 0 ≤ x) (h1 : x ≤ U32.max) :
-  U32.ofInt x (by constructor <;> scalar_tac) ≤ U32.max := by
+  U32.ofIntCore x (by constructor <;> scalar_tac) ≤ U32.max := by
   scalar_tac
 
 -- Not equal
-- 
cgit v1.2.3