Skip to content

Commit

Permalink
chore(category_theory/concrete_category): remove imports (#17093)
Browse files Browse the repository at this point in the history
Remove unneeded imports. This had resulted in someone incorrectly thinking that it was block for porting to mathlib4, so may as well clean up.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
  • Loading branch information
semorrison and semorrison committed Oct 21, 2022
1 parent d5aabe1 commit 6c6597f
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/category_theory/concrete_category/bundled.lean
Expand Up @@ -3,7 +3,7 @@ Copyright (c) 2018 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison, Johannes Hölzl, Reid Barton, Sean Leather
-/
import tactic.pi_instances
import tactic.lint

/-!
# Bundled types
Expand Down

0 comments on commit 6c6597f

Please sign in to comment.