Fix warnings

SSA/Experimental/Bits/AutoStructs/FiniteStateMachine.lean

@@ -21,7 +21,7 @@ variable {α β α' β' : Type} {γ : β → Type}
 where `n` is the number of `BitStream` arguments,
 as a finite state machine.
 -/
-structure FSM (arity : Type) : Type 1 :=
+structure FSM (arity : Type) : Type 1 where
   /--
   The arity of the (finite) type `α` determines how many bits the internal carry state of this
   FSM has -/
@@ -307,7 +307,7 @@ def sub : FSM Bool :=
 theorem carry_sub (x : Bool → BitStream) : ∀ (n : ℕ), sub.carry x (n+1) =
     fun _ => (BitStream.subAux (x true) (x false) n).2
   | 0 => by
-    simp [carry, nextBit, Function.funext_iff, BitStream.subAux, sub]
+    simp [carry, nextBit, BitStream.subAux, sub]
   | n+1 => by
     rw [carry, carry_sub _ n]
     simp [nextBit, eval, sub, BitStream.sub, BitStream.subAux, Bool.xor_not_left']
@@ -333,7 +333,7 @@ def neg : FSM Unit :=
 theorem carry_neg (x : Unit → BitStream) : ∀ (n : ℕ), neg.carry x (n+1) =
     fun _ => (BitStream.negAux (x ()) n).2
   | 0 => by
-    simp [carry, nextBit, Function.funext_iff, BitStream.negAux, neg]
+    simp [carry, nextBit, BitStream.negAux, neg]
   | n+1 => by
     rw [carry, carry_neg _ n]
     simp [nextBit, eval, neg, BitStream.neg, BitStream.negAux, Bool.xor_not_left']
@@ -401,7 +401,7 @@ def ls (b : Bool) : FSM Unit :=
 theorem carry_ls (b : Bool) (x : Unit → BitStream) : ∀ (n : ℕ),
     (ls b).carry x (n+1) = fun _ => x () n
   | 0 => by
-    simp [carry, nextBit, Function.funext_iff, ls]
+    simp [carry, nextBit, ls]
   | n+1 => by
     rw [carry, carry_ls _ _ n]
     simp [nextBit, eval, ls]
@@ -433,7 +433,7 @@ def incr : FSM Unit :=
 theorem carry_incr (x : Unit → BitStream) : ∀ (n : ℕ),
     incr.carry x (n+1) = fun _ => (BitStream.incrAux (x ()) n).2
   | 0 => by
-    simp [carry, nextBit, Function.funext_iff, BitStream.incrAux, incr]
+    simp [carry, nextBit, BitStream.incrAux, incr]
   | n+1 => by
     rw [carry, carry_incr _ n]
     simp [nextBit, eval, incr, incr, BitStream.incrAux]
@@ -456,7 +456,7 @@ def decr : FSM Unit :=
 theorem carry_decr (x : Unit → BitStream) : ∀ (n : ℕ), decr.carry x (n+1) =
     fun _ => (BitStream.decrAux (x ()) n).2
   | 0 => by
-    simp [carry, nextBit, Function.funext_iff, BitStream.decrAux, decr]
+    simp [carry, nextBit, BitStream.decrAux, decr]
   | n+1 => by
     rw [carry, carry_decr _ n]
     simp [nextBit, eval, decr, BitStream.decrAux]
@@ -508,7 +508,7 @@ def repeatBit : FSM Unit where
 
 end FSM
 
-structure FSMSolution (t : Term) extends FSM (Fin t.arity) :=
+structure FSMSolution (t : Term) extends FSM (Fin t.arity) where
   ( good : t.evalFinStream = toFSM.eval )
 
 def composeUnary

SSA/Experimental/Bits/Fast/BitStream.lean

@@ -500,8 +500,9 @@ theorem ofBitVec_one_eqTo_ofNat : @ofBitVec w 1 ≈ʷ ofNat 1 := by
   · simp [EqualUpTo ,h]
   · intros n a
     simp [ofNat_one n, ofBitVec, a]
-    sorry
-    -- omega
+    rw [← Bool.decide_and]
+    rw [decide_eq_decide]
+    omega
 
 theorem ofBitVec_neg : ofBitVec (- x) ≈ʷ - (ofBitVec x) := by
   calc

SSA/Experimental/Bits/Fast/Decide.lean

@@ -8,7 +8,7 @@ instance (t₁ t₂ : Term) : Decidable (t₁.eval = t₂.eval) :=
     ← (termEvalEqFSM (t₁.xor t₂)).good]
   simp only [eval_eq_iff_xor_eq_zero]
   rw [forall_swap]
-  simp only [← Function.funext_iff]
+  simp only [← funext_iff]
 
 
 open Term

SSA/Experimental/Bits/Fast/FiniteStateMachine.lean

@@ -303,7 +303,7 @@ def sub : FSM Bool :=
 theorem carry_sub (x : Bool → BitStream) : ∀ (n : ℕ), sub.carry x (n+1) =
     fun _ => (BitStream.subAux (x true) (x false) n).2
   | 0 => by
-    simp [carry, nextBit, Function.funext_iff, BitStream.subAux, sub]
+    simp [carry, nextBit, funext_iff, BitStream.subAux, sub]
   | n+1 => by
     rw [carry, carry_sub _ n]
     simp [nextBit, eval, sub, BitStream.sub, BitStream.subAux, Bool.xor_not_left']
@@ -329,7 +329,7 @@ def neg : FSM Unit :=
 theorem carry_neg (x : Unit → BitStream) : ∀ (n : ℕ), neg.carry x (n+1) =
     fun _ => (BitStream.negAux (x ()) n).2
   | 0 => by
-    simp [carry, nextBit, Function.funext_iff, BitStream.negAux, neg]
+    simp [carry, nextBit, funext_iff, BitStream.negAux, neg]
   | n+1 => by
     rw [carry, carry_neg _ n]
     simp [nextBit, eval, neg, BitStream.neg, BitStream.negAux, Bool.xor_not_left']
@@ -397,7 +397,7 @@ def ls (b : Bool) : FSM Unit :=
 theorem carry_ls (b : Bool) (x : Unit → BitStream) : ∀ (n : ℕ),
     (ls b).carry x (n+1) = fun _ => x () n
   | 0 => by
-    simp [carry, nextBit, Function.funext_iff, ls]
+    simp [carry, nextBit, funext_iff, ls]
   | n+1 => by
     rw [carry, carry_ls _ _ n]
     simp [nextBit, eval, ls]
@@ -429,7 +429,7 @@ def incr : FSM Unit :=
 theorem carry_incr (x : Unit → BitStream) : ∀ (n : ℕ),
     incr.carry x (n+1) = fun _ => (BitStream.incrAux (x ()) n).2
   | 0 => by
-    simp [carry, nextBit, Function.funext_iff, BitStream.incrAux, incr]
+    simp [carry, nextBit, funext_iff, BitStream.incrAux, incr]
   | n+1 => by
     rw [carry, carry_incr _ n]
     simp [nextBit, eval, incr, incr, BitStream.incrAux]
@@ -452,7 +452,7 @@ def decr : FSM Unit :=
 theorem carry_decr (x : Unit → BitStream) : ∀ (n : ℕ), decr.carry x (n+1) =
     fun _ => (BitStream.decrAux (x ()) n).2
   | 0 => by
-    simp [carry, nextBit, Function.funext_iff, BitStream.decrAux, decr]
+    simp [carry, nextBit, funext_iff, BitStream.decrAux, decr]
   | n+1 => by
     rw [carry, carry_decr _ n]
     simp [nextBit, eval, decr, BitStream.decrAux]

SSA/Experimental/Bits/Fast/Lemmas.lean

@@ -19,11 +19,11 @@ lemma evalFin_eq_eval (t : Term) (vars : Nat → BitStream) :
 
 lemma eq_iff_xor_eq_zero (seq₁ seq₂ : BitStream) :
     (∀ i, seq₁ i = seq₂ i) ↔ (∀ i, (seq₁ ^^^ seq₂) i = BitStream.zero i) := by
-  simp [Function.funext_iff]
+  simp [funext_iff]
 
 lemma eval_eq_iff_xor_eq_zero (t₁ t₂ : Term) :
     t₁.eval = t₂.eval ↔ (t₁.xor t₂).evalFin = fun _ => BitStream.zero := by
-  simp only [Function.funext_iff, Term.eval, Term.evalFin,
+  simp only [funext_iff, Term.eval, Term.evalFin,
     ← eq_iff_xor_eq_zero, ← evalFin_eq_eval]
   constructor
   · intro h seq