From 38ac1b86a8487b13016aafb4d4697992cc5ea4f7 Mon Sep 17 00:00:00 2001 From: RSoulatIOHK Date: Tue, 16 Dec 2025 10:43:51 +0100 Subject: [PATCH] chore: bump to Lean 4.26 Very minimal bump to ensure building and no deprecation warnings --- Blaster/Optimize/Rewriting/OptimizeString.lean | 2 +- lean-toolchain | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Blaster/Optimize/Rewriting/OptimizeString.lean b/Blaster/Optimize/Rewriting/OptimizeString.lean index 48ec885..019ff82 100644 --- a/Blaster/Optimize/Rewriting/OptimizeString.lean +++ b/Blaster/Optimize/Rewriting/OptimizeString.lean @@ -21,7 +21,7 @@ def normStringValue (f : Expr) (args : Array Expr) : TranslateEnvT Expr := do if args.size != 1 then throwEnvError "normStringValue: only one argument expected" let op := args[0]! let some elms ← getListChars? op | return (mkApp f op) - return (mkStrLit (String.mk elms.toList)) + return (mkStrLit (String.ofList elms.toList)) where getListChars? (e : Expr) : MetaM (Option (Array Char)) := do diff --git a/lean-toolchain b/lean-toolchain index e5ab73a..e59446d 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.25.0 +leanprover/lean4:v4.26.0