From afc2a55b20ac1e208ee094fe1104e376f84894bb Mon Sep 17 00:00:00 2001
From: Malvin Gattinger <malvin@w4eg.de>
Date: Tue, 3 Sep 2024 16:20:06 +0200
Subject: [PATCH] add note that PathIn.rewind is probably wrong

---
 Pdl/Soundness.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Pdl/Soundness.lean b/Pdl/Soundness.lean
index a59675a..359db21 100644
--- 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 =>