chore: enable lint in CI

Aesop/Tracing.lean

@@ -31,8 +31,7 @@ namespace TraceOption
 def isEnabled [Monad m] [MonadOptions m] (opt : TraceOption) : m Bool :=
   return opt.option.get (← getOptions)
 
-def withEnabled [Monad m] [MonadWithOptions m] (opt : TraceOption) (k : m α) :
-    m α := do
+def withEnabled [MonadWithOptions m] (opt : TraceOption) (k : m α) : m α :=
   withOptions (λ opts => opt.option.set opts true) k
 
 initialize steps : TraceOption ←

Aesop/Util/Basic.lean

@@ -66,12 +66,12 @@ end PersistentHashSet
 
 -- TODO upstream; generalise to {m : Type u → Type v}.
 -- Need to generalise `HashMap.forM` first.
-scoped instance {m : Type u → Type u} [BEq α] [Hashable α] [Monad m] :
+scoped instance {m : Type u → Type u} [BEq α] [Hashable α] :
     ForM m (HashMap α β) (α × β) where
   forM | m, f => m.forM λ a b => f (a, b)
 
 -- TODO upstream; generalise to {m : Type u → Type v}.
-scoped instance {m : Type u → Type u} [BEq α] [Hashable α] [Monad m] :
+scoped instance {m : Type u → Type u} [BEq α] [Hashable α] :
     ForIn m (HashMap α β) (α × β) where
   forIn := ForM.forIn
 

Aesop/Util/UnorderedArraySet.lean

@@ -45,7 +45,7 @@ protected def ofSortedArray (xs : Array α) : UnorderedArraySet α :=
 
 set_option linter.unusedVariables false in
 /-- O(n*log(n)) -/
-protected def ofArray [ord : Ord α] [Inhabited α] (xs : Array α) :
+protected def ofArray [ord : Ord α] (xs : Array α) :
     UnorderedArraySet α :=
   ⟨xs.sortDedup⟩
 
@@ -91,7 +91,7 @@ def foldM [Monad m] (f : σ → α → m σ) (init : σ) (s : UnorderedArraySet
     m σ :=
   s.rep.foldlM f init
 
-instance [Monad m] : ForIn m (UnorderedArraySet α) α where
+instance : ForIn m (UnorderedArraySet α) α where
   forIn s := s.rep.forIn
 
 /-- O(n) -/

lakefile.toml

@@ -1,6 +1,8 @@
 name = "aesop"
 defaultTargets = ["Aesop"]
 testDriver = "AesopTest"
+lintDriver = "batteries/runLinter"
+lintDriverArgs = ["Aesop"]
 precompileModules = false # We would like to turn this on, but it breaks the Mathlib cache.
 
 [[require]]