DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

change imports

Browse source
This commit is contained in:
jstoobysmith 2024-06-26 08:54:54 -04:00
parent 07e9c65861
commit e389134122
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
scripts/check_file_imports.lean
View file

@ -3,7 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license. Released under Apache 2.0 license.
Authors: Joseph Tooby-Smith Authors: Joseph Tooby-Smith
-/ -/
import HepLean import Batteries.Lean.HashSet
import Lean
/-! /-!
# Check file imports # Check file imports