コードの微修正

lean-ja · Dec 31, 2024 · 756e21b · 756e21b
1 parent 273232b
commit 756e21b
Show file tree

Hide file tree

Showing 5 changed files with 21 additions and 16 deletions.
diff --git a/LeanByExample/Declarative/Infix.lean b/LeanByExample/Declarative/Infix.lean
@@ -57,9 +57,10 @@ open Lean in
 
 /-- マクロを展開するコマンド -/
 elab "#expand " t:macro_stx : command => do
-  let t : Syntax := match t.raw with
-  | .node _ _ #[t] => t
-  | _ => t.raw
+  let t : Syntax :=
+    match t.raw with
+    | .node _ _ #[t] => t
+    | _ => t.raw
   match ← Elab.liftMacroM <| Macro.expandMacro? t with
   | none => logInfo m!"Not a macro"
   | some t => logInfo m!"{t}"

diff --git a/LeanByExample/Declarative/Postfix.lean b/LeanByExample/Declarative/Postfix.lean
@@ -28,9 +28,10 @@ open Lean in
 
 /-- マクロを展開するコマンド -/
 elab "#expand " t:macro_stx : command => do
-  let t : Syntax := match t.raw with
-  | .node _ _ #[t] => t
-  | _ => t.raw
+  let t : Syntax :=
+    match t.raw with
+    | .node _ _ #[t] => t
+    | _ => t.raw
   match ← Elab.liftMacroM <| Macro.expandMacro? t with
   | none => logInfo m!"Not a macro"
   | some t => logInfo m!"{t}"

diff --git a/LeanByExample/Declarative/Prefix.lean b/LeanByExample/Declarative/Prefix.lean
@@ -24,9 +24,10 @@ open Lean in
 
 /-- マクロを展開するコマンド -/
 elab "#expand " t:macro_stx : command => do
-  let t : Syntax := match t.raw with
-  | .node _ _ #[t] => t
-  | _ => t.raw
+  let t : Syntax :=
+    match t.raw with
+    | .node _ _ #[t] => t
+    | _ => t.raw
   match ← Elab.liftMacroM <| Macro.expandMacro? t with
   | none => logInfo m!"Not a macro"
   | some t => logInfo m!"{t}"

diff --git a/LeanByExample/Tactic/Exists.lean b/LeanByExample/Tactic/Exists.lean
@@ -8,7 +8,7 @@ import Lean --#
 example : ∃ x : Nat, 3 * x + 1 = 7 := by
   exists 2
 
-/- ## 内部処理についての補足
+/- ## 舞台裏
 なお Lean での存在量化の定義は次のようになっています。-/
 --#--
 -- Exists の定義が変わっていないことを確認する
@@ -41,9 +41,10 @@ open Lean in
 
 /-- マクロを展開するコマンド -/
 elab "#expand " t:macro_stx : command => do
-  let t : Syntax := match t.raw with
-  | .node _ _ #[t] => t
-  | _ => t.raw
+  let t : Syntax :=
+    match t.raw with
+    | .node _ _ #[t] => t
+    | _ => t.raw
   match ← Elab.liftMacroM <| Macro.expandMacro? t with
   | none => logInfo m!"Not a macro"
   | some t => logInfo m!"{t}"

diff --git a/LeanByExample/Tactic/ShowTerm.lean b/LeanByExample/Tactic/ShowTerm.lean
@@ -32,9 +32,10 @@ open Lean in
 
 /-- マクロを展開するコマンド -/
 elab "#expand " t:macro_stx : command => do
-  let t : Syntax := match t.raw with
-  | .node _ _ #[t] => t
-  | _ => t.raw
+  let t : Syntax :=
+    match t.raw with
+    | .node _ _ #[t] => t
+    | _ => t.raw
   match ← Elab.liftMacroM <| Macro.expandMacro? t with
   | none => logInfo m!"Not a macro"
   | some t => logInfo m!"{t}"