fix imports

leanprover-community · Sep 3, 2024 · 9ee29ce · 9ee29ce
1 parent c0258ef
commit 9ee29ce
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 0 deletions.
diff --git a/ProofWidgets/Cancellable.lean b/ProofWidgets/Cancellable.lean
@@ -1,5 +1,6 @@
 import Lean.Data.Json.FromToJson
 import Lean.Server.Rpc.RequestHandling
+import Std.Data.HashMap
 import ProofWidgets.Compat
 
 /-! Experimental support for cancellable RPC requests.

diff --git a/ProofWidgets/Component/PenroseDiagram.lean b/ProofWidgets/Component/PenroseDiagram.lean
@@ -1,5 +1,6 @@
 import ProofWidgets.Component.Basic
 import ProofWidgets.Data.Html
+import Std.Data.HashMap
 
 namespace ProofWidgets.Penrose
 open Lean Server Std

diff --git a/ProofWidgets/Data/Svg.lean b/ProofWidgets/Data/Svg.lean
@@ -1,4 +1,5 @@
 import ProofWidgets.Data.Html
+import Std.Data.HashMap
 
 namespace ProofWidgets
 open Lean Std