lost again

opencompl · Oct 13, 2024 · 0310101 · 0310101
1 parent 18cc7ab
commit 0310101
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/SSA/Experimental/Bits/Fast/FIniteStateMachineClean.lean b/SSA/Experimental/Bits/Fast/FIniteStateMachineClean.lean
@@ -669,3 +669,6 @@ lemma eval_and (xs : BitStreamProd (Fin 2)) (i : Nat) : and'.eval xs = (xs 0) &&
   --   · simp [h]
   --     sorry
   --   · sorry
+  unfold eval; unfold and'; unfold mkBinaryPredicate
+  simp only [Fin.isValue, Width.n.mk_eq]
+  sorry