fix

leanprover-community · Mar 24, 2024 · 7f50814 · 7f50814
1 parent 10a2177
commit 7f50814
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/ImportGraph/Lean/Name.lean b/ImportGraph/Lean/Name.lean
@@ -64,6 +64,6 @@ returns `ImportGraph`.
 -/
 def getModule (name : Name) (s := "") : Name :=
   match name with
-    | .anonymous => s
+    | .anonymous => .mkSimple s
     | .num _ _ => panic s!"panic in `getModule`: did not expect numerical name: {name}."
     | .str pre s => getModule pre s
diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-03-18
+leanprover/lean4:nightly-2024-03-24
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:nightly-2024-03-18
		leanprover/lean4:nightly-2024-03-24