From d281f43fd5dfeab24fe582fd88564f6c1ab7f934 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 18 Mar 2024 01:39:29 +0100
Subject: Regenerate the constants tests and update Primitives/Base.lean

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

(limited to 'backends/lean/Base')

diff --git a/backends/lean/Base/Primitives/Base.lean b/backends/lean/Base/Primitives/Base.lean
index 0b9d9c39..d2695854 100644
--- a/backends/lean/Base/Primitives/Base.lean
+++ b/backends/lean/Base/Primitives/Base.lean
@@ -69,7 +69,7 @@ def div? {α: Type u} (r: Result α): Bool :=
 def massert (b:Bool) : Result Unit :=
   if b then ret () else fail assertionFailure
 
-def eval_global {α: Type u} (x: Result α) (_: ret? x := by decide): α :=
+def eval_global {α: Type u} (x: Result α) (_: ret? x := by first | apply Eq.refl | decide): α :=
   match x with
   | fail _ | div => by contradiction
   | ret x => x
-- 
cgit v1.2.3


From 59bc33b42009ef3a71b43c844f44cd632476e4fe Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 18 Mar 2024 06:59:11 +0100
Subject: Fix a minor issue

---
 backends/lean/Base/Primitives/Base.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'backends/lean/Base')

diff --git a/backends/lean/Base/Primitives/Base.lean b/backends/lean/Base/Primitives/Base.lean
index d2695854..0c64eca1 100644
--- a/backends/lean/Base/Primitives/Base.lean
+++ b/backends/lean/Base/Primitives/Base.lean
@@ -69,7 +69,9 @@ def div? {α: Type u} (r: Result α): Bool :=
 def massert (b:Bool) : Result Unit :=
   if b then ret () else fail assertionFailure
 
-def eval_global {α: Type u} (x: Result α) (_: ret? x := by first | apply Eq.refl | decide): α :=
+macro "prove_eval_global" : tactic => `(tactic| first | apply Eq.refl | decide)
+
+def eval_global {α: Type u} (x: Result α) (_: ret? x := by prove_eval_global) : α :=
   match x with
   | fail _ | div => by contradiction
   | ret x => x
-- 
cgit v1.2.3