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

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