From b3dd78ff4c8785b6ff9bce9927df90f8c78a9109 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 13 Jun 2024 22:04:13 +0200
Subject: Update Lean to v4.9.0-rc1

---
 backends/lean/Base/Progress/Base.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'backends/lean/Base/Progress/Base.lean')

diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean
index 03c80a42..0e46737f 100644
--- a/backends/lean/Base/Progress/Base.lean
+++ b/backends/lean/Base/Progress/Base.lean
@@ -1,5 +1,4 @@
 import Lean
-import Std.Lean.HashSet
 import Base.Utils
 import Base.Primitives.Base
 import Base.Extensions
@@ -111,7 +110,7 @@ section Methods
       -- Collect all the free variables in the arguments
       let allArgsFVars ← args.foldlM (fun hs arg => getFVarIds arg hs) HashSet.empty
       -- Check if they intersect the fvars we introduced for the existentially quantified variables
-      let evarsSet : HashSet FVarId := HashSet.ofArray (evars.map (fun (x : Expr) => x.fvarId!))
+      let evarsSet : HashSet FVarId := HashSet.empty.insertMany (evars.map (fun (x : Expr) => x.fvarId!))
       let filtArgsFVars := allArgsFVars.toArray.filter (fun var => evarsSet.contains var)
       if filtArgsFVars.isEmpty then pure ()
       else
-- 
cgit v1.2.3