removed unused variables

Saturn/Clause.lean

@@ -37,8 +37,6 @@ theorem contradiction_is_false (n: Nat) : ∀ valuation : Valuation n,
   fun valuation => fun ⟨k, ⟨b, p⟩⟩ =>
     let lem1 : (contradiction n).get k b = none := by rw [contra_at_none n]
     let lem2 : varSat ((contradiction n).get k b) = varSat none := congrArg varSat lem1
-    let lem3 : varSat ((contradiction n).get k b) (valuation.get k b) =
-                varSat none (valuation.get k b) := congr lem2 rfl
     let lem4 : (varSat none (valuation.get k b)) = (none = some (valuation.get k b)) := rfl
     let lem5 : (none = some (valuation.get k b)) := by
       rw [← lem4]
@@ -150,7 +148,7 @@ def someUnitClauseAux {l : Nat} {n : Nat}: (clauses : Vector (Clause (n + 1)) l)
   Option (SomeUnitClause clauses)  :=
     fun clauses posCount negCount cb =>
     match cb with
-    | zero => fun cbBound optCl => optCl
+    | zero => fun _ optCl => optCl
     | m + 1 =>
       fun cbBound optCl =>
       match optCl with

Saturn/Core.lean

@@ -6,7 +6,7 @@ corresponding to its satisfiability. Also a theorem that `isSat` and `isUnsat` a
 exclusive.
 -/
 
-def FinSeq (n: Nat) (α : Type) : Type := (k : Nat) → k < n → α
+@[inline] def FinSeq (n: Nat) (α : Type) : Type := (k : Nat) → k < n → α
 
 inductive Vector (α : Type) : Nat → Type where
   | nil : Vector α zero
@@ -20,9 +20,9 @@ namespace Vector
 def get {α : Type}{n : Nat}(v: Vector α n) : FinSeq n α :=
   fun j jw =>
   match n, v, j, jw with
-  | .(zero), nil, k, lt => nomatch lt
-  | m + 1, cons head tail, zero, lt => head
-  | m + 1, cons head tail, j + 1, w =>  tail.get j (Nat.le_of_succ_le_succ w)
+  | .(zero), nil, _, lt => nomatch lt
+  | _ + 1, cons head _, zero, _ => head
+  | _ + 1, cons _ tail, j + 1, w =>  tail.get j (Nat.le_of_succ_le_succ w)
 end Vector
 
 abbrev Clause(n : Nat) : Type := Vector (Option Bool) n

Saturn/DPLL.lean

@@ -142,7 +142,7 @@ def lengthOneEqual{cl1 cl2 : Clause 1}(eql : cl1.get zero (zero_lt_succ zero) =
                             (funext (fun j =>
                                     match j with
                                     | zero => funext (fun _ => eql)
-                                    | i + 1 => funext (fun jw => nomatch jw)
+                                    | _ + 1 => funext (fun jw => nomatch jw)
                                     ))
 
 def lengthOneUnit{cl: Clause 1}{b : Bool}(eql : cl.get zero (zero_lt_succ zero) = some b):