update import dependencies

m4lvin · Dec 3, 2024 · 2eac927 · 2eac927
1 parent 2c7d1d7
commit 2eac927
Show file tree

Hide file tree

Showing 3 changed files with 214 additions and 181 deletions.
diff --git a/Pdl/Completeness.lean b/Pdl/Completeness.lean
@@ -1,6 +1,7 @@
 -- COMPLETENESS
 
 import Pdl.Soundness
+import Pdl.TableauGame
 import Pdl.Modelgraphs
 
 open HasSat

diff --git a/Pdl/LoadSplit.lean b/Pdl/LoadSplit.lean
@@ -1,6 +1,8 @@
 import Pdl.Syntax
 import Mathlib.Tactic.Use
 
+-- TODO: move all this into Pdl.Syntax
+
 /-! ## Spliting of loaded formulas -/
 
 mutual
@@ -85,7 +87,7 @@ theorem LoadFormula.split_eq_loadMulti_nonEmpty' {δ φ} (lf : LoadFormula)
   rw [this]
 
 theorem loadMulti_nonEmpty_eq_loadMulti :
-    loadMulti_nonEmpty (δ ++ [α]) h φ = loadMulti δ α φ := by -- wrong ?
+    loadMulti_nonEmpty (δ ++ [α]) h φ = loadMulti δ α φ := by
   induction δ
   · simp
   case cons IH =>