Add subproof level check for iff

Mroik · Jul 25, 2024 · 4c23040 · 4c23040
1 parent 4f87287
commit 4c23040
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 3 deletions.
diff --git a/src/app.rs b/src/app.rs
@@ -48,9 +48,7 @@ impl App {
             | State::OrState(OrState::EliminateGetAssumption) => {
                 ("And expression to eliminate", true)
             }
-            State::AndState(AndState::EliminateGetProposition(_)) => {
-                ("Resulting expression", true)
-            }
+            State::AndState(AndState::EliminateGetProposition(_)) => ("Resulting expression", true),
             State::OrState(OrState::EliminateGetLeftSubproof(_))
             | State::OrState(OrState::EliminateGetRightSubproof(_, _))
             | State::ImpliesState(ImpliesState::Introduce)

diff --git a/src/fitch.rs b/src/fitch.rs
@@ -556,6 +556,12 @@ impl Fitch {
             Some(v) => v,
         };
 
+        if self.current_level != self.statements.get(left_sub).unwrap().0 - 1
+            || self.current_level != self.statements.get(right_sub).unwrap().0 - 1
+        {
+            return false;
+        }
+
         if !(left_start == right_end && left_end == right_start) {
             return false;
         }