Bml: compile it all (but still with sorries - is that a word?)

m4lvin · Oct 30, 2023 · a67849b · a67849b
1 parent 1a173d6
commit a67849b
Show file tree

Hide file tree

Showing 3 changed files with 94 additions and 96 deletions.
diff --git a/Bml.lean b/Bml.lean
@@ -1,5 +1,3 @@
--- This module serves as the root of the `Pdl` library.
--- Import modules here that should be built as part of the library.
 import «Bml».Syntax
 import «Bml».Semantics
 import «Bml».Setsimp
@@ -10,5 +8,5 @@ import «Bml».Vocabulary
 import «Bml».Soundness
 import «Bml».Tableauexamples
 import «Bml».Completeness
--- TODO import «Bml».Partitions
--- TODO import «Bml».Interpolation
+import «Bml».Partitions
+import «Bml».Interpolation
diff --git a/Bml/Interpolation.lean b/Bml/Interpolation.lean
@@ -33,4 +33,4 @@ theorem interpolation {ϕ ψ} : Tautology (ϕ↣ψ) → ∃ θ, Interpolant ϕ
   · rw [tautImp_iff_comboNotUnsat]; tauto
   constructor
   · rw [tautImp_iff_comboNotUnsat]; simp at *; tauto
-  · cases pI_prop; unfold voc vocabOfSetFormula at *; simp at *; tauto
+  · cases pI_prop; simp at *; tauto