構文

この章では、Leanにおける構文の宣言とその操作方法について説明します。構文を操作する方法はたくさんあるため、この章ではまだ詳細にあまり深入りせず、ほとんどを後の章に先送りします。

構文の宣言

宣言のためのヘルパー

読者の中には infix や notation コマンドまでもご存じの方もいるかもしれませんが、そうでない方のために簡単におさらいしておきましょう：

import Lean

-- XOR, denoted \oplus
infixl:60 " ⊕ " => fun l r => (!l && r) || (l && !r)

#eval true ⊕ true -- false
#eval true ⊕ false -- true
#eval false ⊕ true -- true
#eval false ⊕ false -- false

-- with `notation`, "left XOR"
notation:10 l:10 " LXOR " r:11 => (!l && r)

#eval true LXOR true -- false
#eval true LXOR false -- false
#eval false LXOR true -- true
#eval false LXOR false -- false

見てわかるように、infixl コマンドによって二項演算の記法を宣言することができます。この二項演算は中置（infix）、つまり演算子がオペランドの間にあることを意味します（これに対して例えば prefix コマンドでは意味が異なります）。infxl の末尾の l は、この記法が左結合であることを意味しており、つまり a ⊕ b ⊕ c は a ⊕ (b ⊕ c) ではなく（これは infixr で実現されます）、(a ⊕ b) ⊕ c とパースされます。このコマンドの右側では、これら2つのパラメータを操作して何らかの値を返す関数を期待しています。一方で、notation コマンドではより自由度が増します：構文定義の中でパラメータをただ「言及」するだけで、右側でそれを操作することができます。これにとどまらず、notation コマンドを使えば、理論的には0から任意の数のパラメータを指定した構文を作ることができます。このためこのコマンドはしばしば「mixfix」記法と呼ばれます。

この2つについて直観的でない部分が2つあります：

  • 演算子の周りに空白を空けていること：「 ⊕ 」、「 LXOR 」。こうすることで、Lean がこれらの構文を後から整形表示する際に、演算子の周りにもスペースを使うようになります。そうしないと構文は l ⊕ r ではなく l⊕r と表示されてしまいます。
  • 60 や 10 などのそれぞれのコマンドの直後にある値は、演算子の優先順位、つまり引数との結合の強さを示しています。このことについて実際の挙動を見てみましょう：
#eval true ⊕ false LXOR false -- false
#eval (true ⊕ false) LXOR false -- false
#eval true ⊕ (false LXOR false) -- true

見てわかるように、Lean のインタプリタは括弧のない最初の項を3つ目の項ではなく2つ目の項と同じようにパースしています。これは ⊕ 記法が LXOR より優先順位が高いため（つまるところ 60 > 10 であるため）、LXOR より先に評価されます。これは * が + の前に評価されるようなルールを実装する方法でもあります。

最後に、この notation の例では、引数に :precedence バインディングがあります：すなわち l:10 と r:11 です。これは左の引数の優先順位が少なくとも 10 以上、右の引数の優先順位が少なくとも 11 以上でなければならないことを意味しています。引数にそれぞれの優先順位を割り当てるには、その引数自体をパースするために使われたルールの優先順位を見ることで行われます。例えば a LXOR b LXOR c を考えてみましょう。理論的にはこれは2つのパースの仕方があります：

  1. (a LXOR b) LXOR c
  2. a LXOR (b LXOR c)

括弧内の引数は優先順位 10 の LXOR ルールによってパースされるため、これらはその外側の LXOR ルールにとっては優先順位 10 の引数として表示されます：

  1. (a LXOR b):10 LXOR c
  2. a LXOR (b LXOR c):10

しかし、LXOR：notation:10 l:10 " LXOR " r:11 の定義をチェックしてみると、右側の引数には少なくとも 11 以上の優先順位が必要であるため、2つ目のパースは不正であり、パース結果は (a LXOR b) LXOR c となり以下が仮定されます：

  • a は 10 以上の優先順位を持つ
  • b は 11 以上の優先順位を持つ
  • c は 11 以上の優先順位を持つ

従って、LXOR は左結合な記法です。読者はこれを右結合にできますか？

注意：ある記法のパラメータに明示的な優先順位が与えられていない場合、それらは暗黙的に優先順位 0 とタグ付けされます。

この節の最後のコメント：Lean は常に可能な限り広いマッチを行おうと試行します。これは3つの重要な意味を持ちます。まず非常に直観的なことですが、ある右結合演算子 ^ があり、Lean が a ^ b ^ c のような式を見た場合、まず a ^ b をパースし、（優先順位が許す限り）これ以上続けられなくなるまでパースを続けようとします。この結果 Lean はこの式を（読者が期待するように）a ^ (b ^ c) とパースします。

第二に、例えば優先順位によって式のどこに括弧が入るかわからないような記法がある場合、例えば以下のような場合を考えます：

notation:65 lhs:65 " ~ " rhs:65 => (lhs - rhs)

a ~ b ~ c のような式は a ~ (b ~ c) としてパースされます。これは Lean が可能な限り広い範囲のパースを見つけようとするからです。一般的な経験則として：優先順位が曖昧な場合、Lean はデフォルトで右結合を使用します。

#eval 5 ~ 3 ~ 3 -- 5 because this is parsed as 5 - (3 - 3)

最後に、下記のような既存のものに被る記法を定義しようとした場合：

-- `a ~ b mod rel` を、ある同値関係 rel に関して a と b が同値であることとして定義
notation:65 a:65 " ~ " b:65 " mod " rel:65 => rel a b

ここで Lean は a ~ b について、先ほどの定義でパースしてしまって mod と関係についての引数をどうしたらよいかわからずにエラーにしてしまうよりも、この記法を利用したいでしょう：

#check 0 ~ 0 mod Eq -- 0 = 0 : Prop

ここでも可能な限り最長のパーサを探すため、mod とその関係についての引数を消費します。

自由形式の構文宣言

上記の infix と notation コマンドを使えば、普通の数学構文を宣言するだけで、すでにかなり遠くまで行けるようになります。しかし、Lean では任意で複雑な構文を導入することもできます。これには syntax と declare_syntax_cat コマンドを使います。syntax コマンドを使うと、既存のいわゆる「構文カテゴリ」に新しい構文ルールを追加することができます。最も一般的な構文カテゴリは以下の通りです：

  • term、このカテゴリについてはエラボレーションの章で詳しく説明しますが、今のところは「値を持つすべてのもののための構文」と考えておけば良いです。
  • command、これは #check や def などのトップレベルコマンドのカテゴリです。
  • TODO: ...

これらを実際に見てみましょう：

syntax "MyTerm" : term

これで 1 + 1 などの代わりに MyTerm と書くことができ、構文的に （syntactically）有効になります。これはコードがコンパイルできる状態であるという意味ではなく、Lean のパーサがそれを理解できるという意味です：

#check_failure MyTerm
-- elaboration function for 'termMyTerm' has not been implemented
--   MyTerm

注意：#check_failure コマンドを使用すると、型付けが正しくない項をエラー無く表示できます。

このいわゆる「エラボレーション関数」の実装は、Lean の基本的な型 Expr の観点からこの構文に実際の意味を与えるものであり、エラボレーションの章で扱う話題です。

notation と infix コマンドは構文宣言とマクロ宣言（マクロについてはマクロの章を参照）を便利にまとめたユーティリティであり、=> の左側の内容で構文を宣言します。前に述べた notation と infix の優先順位に関する原則はすべて syntax にも適用されます。

もちろん、構文木を構築するために、他の構文を独自の宣言に含めることも可能です。例えば、小さな真偽値の表現言語を作ってみることもできます：

namespace Playground2

-- このスコープ修飾子によって、これらの構文宣言がこの `namespace` の中のみに閉じられるようになります。
-- というのもこれらの構文はこの章でこの後も変更するからです。
scoped syntax "⊥" : term -- ⊥ for false
scoped syntax "⊤" : term -- ⊤ for true
scoped syntax:40 term " OR " term : term
scoped syntax:50 term " AND " term : term
#check_failure ⊥ OR (⊤ AND ⊥) -- elaboration function hasn't been implemented but parsing passes

end Playground2

これは機能しますが、AND と OR 演算の左右に任意の項が置けてしまいます。もし構文レベルで真偽値言語だけを受け付けるミニ言語を書きたい場合は、独自の構文カテゴリを宣言する必要があります。これは declare_syntax_cat コマンドを使って行います：

declare_syntax_cat boolean_expr
syntax "⊥" : boolean_expr -- ⊥ for false
syntax "⊤" : boolean_expr -- ⊤ for true
syntax:40 boolean_expr " OR " boolean_expr : boolean_expr
syntax:50 boolean_expr " AND " boolean_expr : boolean_expr

これで独自の構文カテゴリにて作業するようになったため、システムの他の部分とは完全に切り離されました。そして、これらの構文はもはや任意の項で使うことができません：

#check ⊥ AND ⊤ -- expected term

この構文カテゴリをシステムの他の部分に統合するためには、既存の構文を新しい構文で拡張する必要があります。今回の場合は、term のカテゴリに再埋め込みします：

syntax "[Bool|" boolean_expr "]" : term
#check_failure [Bool| ⊥ AND ⊤] -- elaboration function hasn't been implemented but parsing passes

構文コンビネータ

より複雑な構文を宣言するためには、構文に対する基本的な操作がすでに組み込まれていることが望ましいことが多いです。これには以下が含まれます：

  • 構文カテゴリを持たない（つまり拡張できない）補助パーサ
  • 選択肢
  • 繰り返されるパーツ
  • オプショナルなパーツ

これらはすべて構文カテゴリに基づいたエンコーディングを持っていますが、場合によっては非常に不格好になることがあるため、Lean はこれらすべてを簡単に行う方法を提供しています。

これらすべての動作を確認するために、簡単なバイナリ式の構文を定義します。まず初めに、構文カテゴリに属さない名前付きパーサを宣言します。これは普通の def とよく似ています：

syntax binOne := "O"
syntax binZero := "Z"

これらの名前付き構文パーサは上記の構文カテゴリと同じ位置で使用することができますが、構文カテゴリとの唯一の違いは拡張性がないことです。つまり、構文宣言の中で直接展開されるため、適切な構文カテゴリのように新しいパターンを定義することができません。名前付きのパーサには一般的に便利な組み込みがいくつか存在しており、以下は特記に値するものです：

  • 文字列リテラル用の str
  • 数値リテラル用の num
  • 識別子用の ident
  • ... TODO: better list or link to compiler docs

次に数字を理解するパーサを宣言したいです。 2 進数の数字は 0 か 1 であるため、次のように書くことができます：

syntax binDigit := binZero <|> binOne

ここで <|> 演算子は「左右どちらかを受け入れる」動作を実装しています。また、これらを連鎖させて、任意の数・任意の複雑な他の構文を受け入れるパーサを実現することもできます。ここで 2 進数の概念を定義します。通常、 2 進数は数字を直接並べて書きますが、ここでは繰り返しを表現するためにカンマ区切りの表現を使います：

-- 「+」は「1以上」を示す。「0以上」を実現するには代わりに「*」を使う
-- 「,」は `binDigit` の間の区切り文字を示す。もし省略された場合、デフォルトの区切り文字はスペースになる
syntax binNumber := binDigit,+

構文カテゴリの代わりに名前付きパーサを使えばよいため、これを term カテゴリに簡単に追加することができます：

syntax "bin(" binNumber ")" : term
#check bin(Z, O, Z, Z, O) -- elaboration function hasn't been implemented but parsing passes
#check bin() -- fails to parse because `binNumber` is "one or many": expected 'O' or 'Z'

syntax binNumber' := binDigit,* -- note the *
syntax "emptyBin(" binNumber' ")" : term
#check_failure emptyBin() -- elaboration function hasn't been implemented but parsing passes

パーサごとに 1 つの構文コンビネータしか使えないという制限は一切ないことに注意してください。これらをすべてインラインに記述することも可能です：

syntax "binCompact(" ("Z" <|> "O"),+ ")" : term
#check_failure binCompact(Z, O, Z, Z, O) -- elaboration function hasn't been implemented but parsing passes

最後の機能として、宣言されている 2 進数リテラルを説明するオプションの文字列コメントを追加しましょう：

-- (...)? 構文は括弧内がオプショナルであることを意味します
syntax "binDoc(" (str ";")? binNumber ")" : term
#check_failure binDoc(Z, O, Z, Z, O) -- elaboration function hasn't been implemented but parsing passes
#check_failure binDoc("mycomment"; Z, O, Z, Z, O) -- elaboration function hasn't been implemented but parsing passes

構文に対する操作

上記で説明したように、この章では構文に与えたい意味を Lean に伝える方法については詳しく触れません。しかし、構文を操作する関数の書き方については見ていきます。Lean での他のものと同様に、構文は Lean.Syntax という帰納型によって表現されています。これによって構文を操作することが可能です。この型にはかなり多くの情報が含まれていますが、興味があることのほとんどは次のように単純化できます：

namespace Playground2

inductive Syntax where
  | missing : Syntax
  | node (kind : Lean.SyntaxNodeKind) (args : Array Syntax) : Syntax
  | atom : String -> Syntax
  | ident : Lean.Name -> Syntax

end Playground2

コンストラクタの定義を1つずつ見ていきましょう：

  • missing は Lean のコンパイラによってパースできないようなものがある際に使われます。このおかげで Lean はファイルの一部で構文エラーがあっても、そこから回復してファイルの残りの部分を理解しようとします。これはまた、このコンストラクタはあまり気にされないものであるということでもあります。
  • node は名前の通り、構文木のノードです。ノードは kind : SyntaxNodeKind と呼ばれるものを持っています。この SyntaxNodeKind はただの Lean.Name です。基本的に、各 syntax 宣言は自動的に生成された SyntaxNodeKind を受け取り（この名前は syntax (name := foo) ... : cat で明示的に指定することもできます）、これによって Lean に「この関数は特定の構文構築を行う責任がある」ということを伝えます。さらに、木の中の全てのノードと同様に、この関数にも子があり、この場合は Array Syntax をいう形式をとっています。
  • atom は（1つを除いて）階層の一番下にあるすべての構文オブジェクトを表します。例えば、上の演算子 ⊕ と LXOR は atom として表現されます。
  • ident は atom で前述したこのルールの例外です。ident と atom の違いは実に明白です：識別子はそれを表すにあたって String の代わりに Lean.Name を持ちます。なぜ Lean.Name が単なる String ではないのかはマクロの章で詳しく説明するマクロの健全性（macro hygiene）と呼ばれる概念に関連しています。今のところ、これらは基本的に等価であると考えることができます。

新しい Syntax の構築

Lean で構文がどのように表現されるか学んだので、もちろんのことながらこれらの帰納的な木をすべて手作業で生成するプログラムを書くことができますが、これは恐ろしく退屈であり間違いなく最高に避けたい作業です。幸運なことに、Lean.Syntax 名前空間には非常に広範囲な API が秘められています：

open Lean
#check Syntax -- Syntax. autocomplete

Syntax を作るための興味深い関数は Syntax.mk* で、identのような基本的な Syntax オブジェクトの作成だけでなく、 Syntax.mkApp による複雑なオブジェクトも作成することができます。Syntax.mkApp によって、第1引数の関数を第2引数の引数リスト（すべて Syntax として与えられます）に適用することに相当する Syntax オブジェクトを作成することができます。いくつか例を見てみましょう：

-- 名前のリテラルは名前の前にちょっと ` を付けて書きます
#eval Syntax.mkApp (mkIdent `Nat.add) #[Syntax.mkNumLit "1", Syntax.mkNumLit "1"] -- is the syntax of `Nat.add 1 1`
#eval mkNode `«term_+_» #[Syntax.mkNumLit "1", mkAtom "+", Syntax.mkNumLit "1"] -- is the syntax for `1 + 1`

-- `«term_+_» は + の構文用に自動生成された SyntaxNodeKind であることに注意

もし読者が Syntax を作成するこの方法を全く好まないのあれば、著者も全く同感です。しかし、これを綺麗で正しい方法で行うための機構（上記の機構はだいたい正しい部分を担います）は、マクロの章でもいくつか説明します。

Syntax に対するマッチ

Syntax の構築が重要なトピックであるように、特にマクロでは構文のマッチも同様に（あるいは実はそれ以上に）興味深いものです。幸運なことに、帰納型自体でマッチする必要はありません：その代わりにいわゆる「構文パターン」を使います。これらは非常にシンプルで、その構文はただ `(the syntax I want to match on) とするだけです。実際に使ってみましょう：

def isAdd11 : Syntax → Bool
  | `(Nat.add 1 1) => true
  | _ => false

#eval isAdd11 (Syntax.mkApp (mkIdent `Nat.add) #[Syntax.mkNumLit "1", Syntax.mkNumLit "1"]) -- true
#eval isAdd11 (Syntax.mkApp (mkIdent `Nat.add) #[mkIdent `foo, Syntax.mkNumLit "1"]) -- false

マッチの次のレベルはリテラルにマッチするだけでなく、入力から変数をキャプチャすることです。これは少しファンシーな見た目の構文で行われます：

def isAdd : Syntax → Option (Syntax × Syntax)
  | `(Nat.add $x $y) => some (x, y)
  | _ => none

#eval isAdd (Syntax.mkApp (mkIdent `Nat.add) #[Syntax.mkNumLit "1", Syntax.mkNumLit "1"]) -- some ...
#eval isAdd (Syntax.mkApp (mkIdent `Nat.add) #[mkIdent `foo, Syntax.mkNumLit "1"]) -- some ...
#eval isAdd (Syntax.mkApp (mkIdent `Nat.add) #[mkIdent `foo]) -- none

型付けされた構文

この例の x と y は Syntax ではなく TSyntax `term 型であることに注意してください。コンストラクタを見ればわかるように、完璧に TSyntax ではない型だけで構成されている Syntax に対してパターンマッチしたのにも関わらずにこうなってしまっているのは、いったい何が起こっているのでしょうか？基本的に、`() 構文は賢いため、マッチする構文からくる可能性のあるもの（この場合は term）の中で最も一般的な構文カテゴリを把握することができます。この時に型付けされた構文型 TSyntax が用いられます。これはそれのもとになった構文カテゴリの Name でパラメータ化されています。これはプログラマにとって何が起こっているのかを確認するために便利なだけでなく、他にも利点があります。例えば、次の例で構文カテゴリを num に限定すると、Lean はパターンマッチやパニックのオプション無しで、結果の TSyntax `num に対して直接 getNat を呼び出すことができます：

-- ここで項の構文を操作する関数を明示的にマークしている
def isLitAdd : TSyntax `term → Option Nat
  | `(Nat.add $x:num $y:num) => some (x.getNat + y.getNat)
  | _ => none

#eval isLitAdd (Syntax.mkApp (mkIdent `Nat.add) #[Syntax.mkNumLit "1", Syntax.mkNumLit "1"]) -- some 2
#eval isLitAdd (Syntax.mkApp (mkIdent `Nat.add) #[mkIdent `foo, Syntax.mkNumLit "1"]) -- none

TSyntax の裏にある Syntax にアクセスしたい場合は、TSyntax.raw で可能ですが、ほとんどの場合は型強制でうまくいきます。その他の TSyntax システムの恩恵についてはマクロの章で見ていきます。

構文の機構について最後に大事な注意を：この基本的な形式では、term カテゴリからの構文にのみしか機能しません。これを自前の構文カテゴリに使いたい場合は `(category| ...) を使う必要があります。

ミニプロジェクト

本章での最後のミニプロジェクトとして、算術式についての小さな言語の構文とそれを評価する Syntax → Nat 型の関数を定義します。以下のコンセプトについては今後の章でさらに見ていきます。

declare_syntax_cat arith

syntax num : arith
syntax arith "-" arith : arith
syntax arith "+" arith : arith
syntax "(" arith ")" : arith

partial def denoteArith : TSyntax `arith → Nat
  | `(arith| $x:num) => x.getNat
  | `(arith| $x:arith + $y:arith) => denoteArith x + denoteArith y
  | `(arith| $x:arith - $y:arith) => denoteArith x - denoteArith y
  | `(arith| ($x:arith)) => denoteArith x
  | _ => 0

-- Elab.TermElabM は無視することができる。
-- ここで重要なことは、 `Syntax` を構築するにあたって以下のようにマッチすることができるだけでなく
-- ``(arith| (12 + 3) - 4)` という記法を使うことができる。
def test : Elab.TermElabM Nat := do
  let stx ← `(arith| (12 + 3) - 4)
  pure (denoteArith stx)

#eval test -- 11

この例を自由に弄って好きなように拡張してみてください。次の章では、主に Syntax を何らかの方法で操作する関数について説明します。

エラボレートのさらなる例

記法のための型クラスの利用

構文システムの代わりに、型システムを通じた記法を追加するために型クラスを使うことができます。これは例えば、型クラス HAdd と Add を使った + や、など Lean のその他の共通の演算子の一般的な定義方法などです。

例えば、部分集合記法のための一般的な記法が欲しいとしましょう。まず初めにすべきことは、この記法を確立したい関数を備えた型クラスを定義することです。

class Subset (α : Type u) where
  subset : α → α → Prop

次のステップは記法の定義です。ここでできることは、単純にコード中に現れる ⊆ のインスタンスをすべて Subset.subset の呼び出しに置き換えることです。というのも型クラスの解決によってどの Subset インスタンスが参照されているかを把握することができるからです。したがって記法はシンプルになります：

-- この例の優先順位は任意
infix:50 " ⊆ " => Subset.subset

これを検証するために簡単な集合論を定義してみましょう：

-- `Set` はそれを保持する要素によって定義される
-- -> その要素の型に対するシンプルな述語
def Set (α : Type u) := α → Prop

def Set.mem (x : α) (X : Set α) : Prop := X x

-- 既存の要素の所属の記法の型クラスへと統合
instance : Membership α (Set α) where
  mem := Set.mem

def Set.empty : Set α := λ _ => False

instance : Subset (Set α) where
  subset X Y := ∀ (x : α), x ∈ X → x ∈ Y

example : ∀ (X : Set α), Set.empty ⊆ X := by
  intro X x
  -- ⊢ x ∈ Set.empty → x ∈ X
  intro h
  exact False.elim h -- empty set has no members

束縛子

変数の束縛子を使用する構文を宣言することは Lean 3 ではかなり非直観的でしたが、Lean 4 ではどのように自然にできるかを簡単に見てみましょう。

この例では、ある性質が成り立つようなすべての要素 x を含む集合のよく知られた記法を定義します：例えば {x ∈ ℕ | x < 10} です。

まず最初に、上記の集合論を少し拡張する必要があります：

-- 「～であるようなすべての要素」という基本的な関数のための記法
def setOf {α : Type} (p : α → Prop) : Set α := p

この関数を用いて、この記法の基本的なバージョンを直観的に定義することができます：

notation "{ " x " | " p " }" => setOf (fun x => p)

#check { (x : Nat) | x ≤ 1 } -- { x | x ≤ 1 } : Set Nat

example : 1 ∈ { (y : Nat) | y ≤ 1 } := by simp[Membership.mem, Set.mem, setOf]
example : 2 ∈ { (y : Nat) | y ≤ 3 ∧ 1 ≤ y } := by simp[Membership.mem, Set.mem, setOf]

この直観的な記法は期待通りの形で渡されるものに対処することができます。

この記法を拡張して {x ∈ X | p x} のような集合論的な書き方を許可し、束縛変数の周りの括弧を省く方法についてはマクロの章を参照してください。

演習問題

  1. 5 * 8 💀 4 が 20 を、8 💀 6 💀 1 が 3 を返すような「緊急マイナス 💀」記法を作ってください。

    a) notation コマンドを使う場合。 b) infix コマンドを使う場合。 c) syntax コマンドを使う場合。

    ヒント：Lean 4 の乗算は infixl:70 " * " => HMul.hMul で定義されています。

  2. 以下の構文カテゴリを考えてみましょう：term・command・tactic；そして以下に示す 3 つの構文ルールについて、これらの新しく定義された構文をそれぞれ使ってみましょう。

      syntax "good morning" : term
  syntax "hello" : command
  syntax "yellow" : tactic

  3. 以下のコマンドを許容する syntax ルールを作ってください：

    • red red red 4
    • blue 7
    • blue blue blue blue blue 18

    （つまり、複数の red の後に数字が来るか；あるいは複数の blue の後に数字が来るか；red blue blue 5 は機能しません。）

    以下のコードテンプレートを使用してください：

    syntax (name := colors) ...
-- our "elaboration function" that infuses syntax with semantics
@[command_elab colors] def elabColors : CommandElab := λ stx => Lean.logInfo "success!"

  4. Mathlib には #help option コマンドがあり、現在の環境で利用可能なすべてのオプションとその説明を表示します。#help option pp.r は部分文字列「pp.r」で始まるすべてのオプションを表示します。

    以下のコマンドを許容する syntax ルールを作ってください：

    • #better_help option
    • #better_help option pp.r
    • #better_help option some.other.name

    以下のテンプレートを使用してください：

    syntax (name := help) ...
-- our "elaboration function" that infuses syntax with semantics
@[command_elab help] def elabHelp : CommandElab := λ stx => Lean.logInfo "success!"

  5. Mathlib には ∑ 演算子があります。以下の項を許容する syntax ルールを作ってください：

    • ∑ x in { 1, 2, 3 }, x^2
    • ∑ x in { "apple", "banana", "cherry" }, x.length

    以下のテンプレートを使用してください：

    import Std.Classes.SetNotation
import Std.Util.ExtendedBinder
syntax (name := bigsumin) ...
-- our "elaboration function" that infuses syntax with semantics
@[term_elab bigsumin] def elabSum : TermElab := λ stx tp => return mkNatLit 666

    ヒント：Std.ExtendedBinder.extBinder パーサを使ってください。 ヒント：これらの import を機能させるには読者の Lean プロジェクトに batteries をインストールする必要があります。