From e3891341225f0579e4695e2f75ac24f8f4c016b3 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Wed, 26 Jun 2024 08:54:54 -0400 Subject: [PATCH] change imports --- scripts/check_file_imports.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/scripts/check_file_imports.lean b/scripts/check_file_imports.lean index bbc552c..ec21e44 100644 --- a/scripts/check_file_imports.lean +++ b/scripts/check_file_imports.lean @@ -3,7 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license. Authors: Joseph Tooby-Smith -/ -import HepLean +import Batteries.Lean.HashSet +import Lean /-! # Check file imports