tmp

opencompl · Oct 1, 2024 · 2311e78 · 2311e78
1 parent 888925b
commit 2311e78
Showing 1 changed file with 3 additions and 3 deletions.
diff --git 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