リンターオプションを追加する

LeanByExample/Reference/Tactic/Induction.lean

@@ -124,7 +124,7 @@ example (n : Nat) : fibonacci n = fib n := by
 
       -- 帰納法の仮定から、`n` と `n + 1` については成り立つ
       have ih_n := ih n
-      have ih_succ := ih $ n + 1
+      have ih_succ := ih (n + 1)
 
       -- 帰納法の仮定を適用して示す
       simp [ih_n, ih_succ]
@@ -146,7 +146,7 @@ theorem fib_eq (n : Nat) : fibonacci n = fib n := by
 
     -- 帰納法の仮定から、`n` と `n + 1` については成り立つ
     have ih_n := fib_eq n
-    have ih_succ := fib_eq $ n + 1
+    have ih_succ := fib_eq (n + 1)
 
     -- 帰納法の仮定を適用して示す
     simp [ih_n, ih_succ]

LeanByExample/Tutorial/Exercise/HeytingAndBooleanAlgebra.lean

@@ -71,6 +71,7 @@ class Semilatticeinf (α : Type) extends Inf α, PartialOrder α where
   /-- `a ⊓ b` は `a`, `b` の下界の中で最大のもの -/
   le_inf : ∀ a b c : α, c ≤ a → c ≤ b → c ≤ a ⊓ b
 
+set_option structureDiamondWarning false in --#
 /-- 束 -/
 class Lattice (α : Type) extends SemilatticeSup α, Semilatticeinf α
 

LeanByExample/Tutorial/Solution/HeytingAndBooleanAlgebra.lean

@@ -71,6 +71,7 @@ class Semilatticeinf (α : Type) extends Inf α, PartialOrder α where
   /-- `a ⊓ b` は `a`, `b` の下界の中で最大のもの -/
   le_inf : ∀ a b c : α, c ≤ a → c ≤ b → c ≤ a ⊓ b
 
+set_option structureDiamondWarning false in --#
 /-- 束 -/
 class Lattice (α : Type) extends SemilatticeSup α, Semilatticeinf α
 

lakefile.lean

@@ -1,15 +1,22 @@
 import Lake
 open Lake DSL
 
+abbrev linterOptions : Array LeanOption := #[
+  ⟨`linter.flexible, true⟩,
+  ⟨`linter.oldObtain, true⟩,
+  ⟨`linter.style.cdot, true⟩,
+  ⟨`linter.style.dollarSyntax, true⟩,
+  ⟨`linter.style.missingEnd, true⟩,
+  ⟨`linter.style.lambdaSyntax, true⟩,
+  ⟨`structureDiamondWarning, true⟩
+]
+
 package «Lean by Example» where
   leanOptions := #[
     ⟨`autoImplicit, false⟩,
-    ⟨`relaxedAutoImplicit, false⟩,
-    ⟨`weak.linter.flexible, true⟩
-  ]
-  moreServerOptions := #[
-    ⟨`linter.flexible, true⟩
-  ]
+    ⟨`relaxedAutoImplicit, false⟩
+  ] ++ linterOptions.map (fun s ↦ {s with name := `weak ++ s.name})
+  moreServerOptions := linterOptions
 
 require «mk-exercise» from git
   "https://github.com/Seasawher/mk-exercise.git" @ "main"