From 1f507168c6bef1abc5201270f5428e855fc929b8 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Fri, 22 Mar 2024 14:49:02 +1100 Subject: [PATCH] chore: bump for compatibility with Std --- ImportGraph/Lean/Name.lean | 1 + lake-manifest.json | 2 +- lean-toolchain | 2 +- 3 files changed, 3 insertions(+), 2 deletions(-) diff --git a/ImportGraph/Lean/Name.lean b/ImportGraph/Lean/Name.lean index 00d5896..49a0fe0 100644 --- a/ImportGraph/Lean/Name.lean +++ b/ImportGraph/Lean/Name.lean @@ -8,6 +8,7 @@ import Lean.CoreM import Std.Data.HashMap.Basic import Std.Lean.Name import Std.Lean.SMap +import Lean.Meta.Match.MatcherInfo /-! TODO: Some declarations in this file are duplicated from mathlib, but especially `isBlacklisted` diff --git a/lake-manifest.json b/lake-manifest.json index 9253fb2..fdcaf4a 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -13,7 +13,7 @@ {"url": "https://github.com/leanprover/std4", "type": "git", "subDir": null, - "rev": "2a1b7546b2df0f8e65a70d3b228c30d91752acc4", + "rev": "0783e9ceae1c8c11957fb5e0fe3e70fd2d43eea2", "name": "std", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lean-toolchain b/lean-toolchain index f96d662..e35881c 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.6.1 +leanprover/lean4:v4.7.0-rc2