Merge pull request #437 from lean-ja/Seasawher/issue226

コマンド紹介: infix を紹介する

Author: Seasawher

.lycheeignore

@@ -1,2 +1,3 @@
 https://raw.githubusercontent.com/lean-ja/lean-by-example/.*
 https://adam.math.hhu.de/#/g/leanprover-community/NNG4
+https://live.lean-lang.org/

Examples/Command/Declarative/Infix.lean

@@ -0,0 +1,44 @@
+/- # infix
+`infix` は，中置記法を定義する構文です．
+-/
+import Lean --#
+namespace Infix --#
+
+-- 中置記法を定義. 中身はただの掛け算
+-- 特定の名前空間でだけ有効にするために `scoped` を付けている
+scoped infix:60 " ⋄ " => Nat.mul
+
+#guard 2 ⋄ 3 = 6
+
+/- `:` の後に付けている数字はパースの優先順位で，高いほど結合するタイミングが早くなります．等号 `=` の優先順位は 50 であることを覚えておくと良いかもしれません．-/
+
+-- 等号より微妙に優先順位が高い
+scoped infix:51 " strong " => Nat.add
+
+-- きちんと 1 + (2 strong 3) = 6 と解釈される．
+-- これは， 等号の優先順位が 51 未満であることを意味する
+#check 1 + 2 strong 3 = 6
+
+-- 優先順位を 50 より小さくすると等号より優先順位が低くなる
+-- したがってエラーになる
+scoped infix:49 " weak " => Nat.add
+
+#check_failure 1 + 2 weak 3 = 6
+
+/- ## 舞台裏
+
+`infix` は [`notation`](./Notation.md) コマンドの特別な場合であり，実際内部的にはマクロとして展開されます．以下の例では，`infix:50 " LXOR " => fun l r => (!l && r)` が `notation:50 lhs:51 " LXOR " rhs:51 => (fun l r => (!l && r)) lhs rhs` とマクロ展開されていることがわかります．-/
+
+open Lean
+
+/-- コマンドをマクロ展開するコマンド -/
+elab "#expand_command " t:command : command => do
+  match ← Elab.liftMacroM <| Lean.Macro.expandMacro? t with
+  | none => logInfo m!"Not a macro"
+  | some t =>
+    logInfo m!"{t}"
+
+/-- info: notation:50 lhs✝:51 " LXOR " rhs✝:51 => (fun l r => (!l && r)) lhs✝ rhs✝ -/
+#guard_msgs in #expand_command infix:50 " LXOR " => fun l r => (!l && r)
+
+end Infix --#

src/SUMMARY.md

@@ -30,6 +30,7 @@
     - [example: 名前をつけずに証明](./Command/Declarative/Example.md)
     - [export: 現在の名前空間に追加](./Command/Declarative/Export.md)
     - [inductive: 帰納型を定義する](./Command/Declarative/Inductive.md)
+    - [infix: 中置記法](./Command/Declarative/Infix.md)
     - [instance: インスタンスを定義する](./Command/Declarative/Instance.md)
     - [local: 有効範囲をセクションで限定](./Command/Declarative/Local.md)
     - [namespace: 名前空間を宣言する](./Command/Declarative/Namespace.md)