add note that PathIn.rewind is probably wrong

m4lvin · Sep 3, 2024 · afc2a55 · afc2a55
1 parent 2826949
commit afc2a55
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/Pdl/Soundness.lean b/Pdl/Soundness.lean
@@ -438,6 +438,7 @@ theorem PathIn.prefix_toList_eq_toList_take {tab : Tableau Hist X}
 
 /-- Rewinding a path, removing the last `k` steps. Cannot go into Hist.
 Used to go to the companion of a repeat. -/
+-- PROBLEM: this definition seems to be wrong!
 def PathIn.rewind : (t : PathIn tab) → (k : Fin (t.toHistory.length + 1)) → PathIn tab
 | .nil, _ => .nil
 | .loc Y_in tail, k =>