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