fix(Model): Add Morphism.lean for build target (iehality#35)

FormalMathematicsLab · Apr 5, 2024 · 453bf65 · 453bf65
1 parent 00a81cf
commit 453bf65
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 2 deletions.
diff --git a/Logic/Modal/Normal.lean b/Logic/Modal/Normal.lean
@@ -8,6 +8,7 @@ import Logic.Modal.Normal.Soundness
 import Logic.Modal.Normal.Completeness
 import Logic.Modal.Normal.ModalCube
 import Logic.Modal.Normal.ModalCompanion
+import Logic.Modal.Normal.Morphism
 
 import Logic.Modal.Normal.GL.Semantics
 import Logic.Modal.Normal.GL.Soundness
diff --git a/Logic/Modal/Normal/Irreflexive.lean → Logic/Modal/Normal/Morphism.lean b/Logic/Modal/Normal/Irreflexive.lean → Logic/Modal/Normal/Morphism.lean
@@ -1,5 +1,3 @@
-import Logic.Modal.Normal.Formula
-import Logic.Modal.Normal.Deduction
 import Logic.Modal.Normal.Semantics
 
 namespace LO.Modal.Normal