Skip to content

Commit c7cff45

Browse files
fgdoraisJLimperg
authored andcommittedNov 20, 2023
chore: fix imports
1 parent 0b14a4d commit c7cff45

File tree

3 files changed

+3
-2
lines changed

3 files changed

+3
-2
lines changed
 

‎Aesop/Script.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ import Aesop.Util.EqualUpToIds
1010
import Std.Lean.Meta.Clear
1111
import Std.Lean.Meta.Inaccessible
1212
import Std.Lean.HashSet
13+
import Std.Tactic.Ext
1314

1415
open Lean
1516
open Lean.Elab.Tactic

‎Aesop/Search/Queue.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ import Aesop.Options
88
import Aesop.Tracing
99
import Aesop.Tree
1010
import Aesop.Search.Queue.Class
11-
import Std.Data.BinomialHeap
11+
import Std.Data.BinomialHeap.Basic
1212

1313
open Lean
1414
open Std (BinomialHeap)

‎Aesop/Util/UnionFind.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Jannis Limperg
55
-/
66

7-
import Std.Data.HashMap
7+
import Std.Data.HashMap.Basic
88

99
open Std (HashMap)
1010

0 commit comments

Comments
 (0)