From 2311e7801958493d6ea03a56f995c6eb7478d854 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Tue, 1 Oct 2024 17:51:55 +0100 Subject: [PATCH] tmp --- SSA/Experimental/Bits/Fast/FiniteStateMachine.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/SSA/Experimental/Bits/Fast/FiniteStateMachine.lean b/SSA/Experimental/Bits/Fast/FiniteStateMachine.lean index 44b620eb4..f498a084d 100644 --- a/SSA/Experimental/Bits/Fast/FiniteStateMachine.lean +++ b/SSA/Experimental/Bits/Fast/FiniteStateMachine.lean @@ -453,12 +453,12 @@ def mapCircuit (c : Circuit (Fin n)) : FSM n where case zero => simp [eval.next, next, BitVec.zero_width_append _, BitStream.head] case succ m ih => - simp [eval.next] specialize ih xs.tails - simp at ih - rw [ih (xs.tails)] + -- rw [ih (xs.tails)] + + sorry