diff --git a/ImportGraph/CurrentModule.lean b/ImportGraph/CurrentModule.lean index 55edecd..94a5aec 100644 --- a/ImportGraph/CurrentModule.lean +++ b/ImportGraph/CurrentModule.lean @@ -5,7 +5,7 @@ Authors: Jon Eugster -/ import Lake.Load.Manifest -open Lake +open Lean (Name) namespace ImportGraph diff --git a/lean-toolchain b/lean-toolchain index 22d46f9..d23c674 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-10-17 +leanprover/lean4:nightly-2024-10-21