6.1. 識別子（Identifiers）

syntaxIdentifiers
$x:ident

識別子の項は名前への参照です。 識別子についての具体的なレキシカル構文は Lean での具体的な構文の節 で説明されています。 Lean.Parser.Term.let : term`let` is used to declare a local definition. Example: ``` let x := 1 let y := x + 1 x + y ``` Since functions are first class citizens in Lean, you can use `let` to declare local functions too. ``` let double := fun x => 2*x double (double 3) ``` For recursive definitions, you should use `let rec`. You can also perform pattern matching using `let`. For example, assume `p` has type `Nat × Nat`, then you can write ``` let (x, y) := p x + y ``` let や Lean.Parser.Term.fun : termfun のように、識別子は名前を束縛するコンテキストでも出現します；しかし、この場合の束縛の出現はそれらだけでは完全な項にはなりません。識別子から名前へのマッピングは自明ではありません： module 内の任意のポイントでも、 namespaces を開くことができ、そこでは セクション変数 やローカルの束縛があるかもしれません。さらに、識別子はドットで区切られた複数のアトミック識別子を含むことがあります；ドットは名前空間とその内容、または変数と フィールド記法 を使用するフィールドまたは関数の両方を区切ります。これはあいまいさを生みます。なぜなら、識別子 A.B.C.D.e.f は以下のいずれかを指す可能性があるからです：

  • 名前空間 A.B.C.D.e にある名前 f（例えば、e の Lean.Parser.Command.declaration : commandwhere ブロックで定義された関数）

  • A.B.C.D.e が T 型を持つ場合、T.f の A.B.C.D.e への適用

  • 構造体 A.B.C.D.e からのフィールド f の射影

  • 構造体の値 A から一連のフィールド射影の列 B.C.D.e を適用し、フィールド記法を用いて f を適用したもの

  • 名前空間 Q が開いている場合は Q 接頭辞を持つ任意を参照できるため、Q.A.B.C.D.e に含まれる名前 f など

このリストは網羅的ではありません。識別子が与えられると、エラボレータは識別子がどの名前（複数の場合もある）を参照しているのか、後続のコンポーネントのフィールドかフィールド記法で適用される関数なのかを発見しなければなりません。これは名前 解決 （resolve）と呼ばれます。

グローバル環境内のいくつかの宣言は、最初に参照された時に遅延して作成されます。これらの宣言の1つを作成し、その宣言を参照するように識別子を解決することを名前の 実現 （realizing）と呼びます。名前解決と名前実現の規則は同じであるため、この節では名前解決のみに言及しますが、両方に適用されます。

名前解決は以下の影響を受けます：

  • 識別子にアタッチされた 事前解決された名前

  • 識別子にアタッチされた マクロスコープ

  • Lean.Parser.Term.letrec : termlet rec のエラボレーションの一部として作成された補助定義を含む、スコープ内のローカル束縛

  • 現在のモジュールによってインポートされたモジュール内で Lean.Parser.Command.export : commandAdds names from other namespaces to the current namespace. The command `export Some.Namespace (name₁ name₂)` makes `name₁` and `name₂`: - visible in the current namespace without prefix `Some.Namespace`, like `open`, and - visible from outside the current namespace `N` as `N.name₁` and `N.name₂`. ## Examples ```lean namespace Morning.Sky def star := "venus" end Morning.Sky namespace Evening.Sky export Morning.Sky (star) -- `star` is now in scope #check star end Evening.Sky -- `star` is visible in `Evening.Sky` #check Evening.Sky.star ``` export で作成されたエイリアス

  • 現在の セクションスコープ 、特に、現在の名前空間・開いている名前空間・セクション変数

識別子のどの接頭辞も一連の名前へ解決することができます。解決プロセスに含まれなかった接尾辞は、フィールドの射影またはフィールド記法として扱われます。接頭辞は短いものより長いものの解決が優先されます；言い換えれば、識別子のできるだけ少ない構成要素がフィールド記法として扱われます。識別子の接頭辞は上から優先的に以下のいずれかを指すことがあります：

  1. 識別子の接頭辞と同じ名前を持つローカル束縛変数。これはマクロスコープを含め、最も近いローカル束縛がそれより外側のものよりも優先されます。

  2. 識別子の接頭辞と同じ名前を持つローカルの補助定義

  3. 識別子の接頭辞と同じ名前を持つ セクション変数

  4. 現在の名前空間 の接頭辞に識別子の接頭辞を付加したものと同じグローバル名、または現在の名前空間の接頭辞にエイリアスが存在するもの。これは現在の名前空間においてより長い接頭辞が短いものよりも優先されます。

  5. Lean.Parser.Command.open : commandMakes names from other namespaces visible without writing the namespace prefix. Names that are made available with `open` are visible within the current `section` or `namespace` block. This makes referring to (type) definitions and theorems easier, but note that it can also make [scoped instances], notations, and attributes from a different namespace available. The `open` command can be used in a few different ways: * `open Some.Namespace.Path1 Some.Namespace.Path2` makes all non-protected names in `Some.Namespace.Path1` and `Some.Namespace.Path2` available without the prefix, so that `Some.Namespace.Path1.x` and `Some.Namespace.Path2.y` can be referred to by writing only `x` and `y`. * `open Some.Namespace.Path hiding def1 def2` opens all non-protected names in `Some.Namespace.Path` except `def1` and `def2`. * `open Some.Namespace.Path (def1 def2)` only makes `Some.Namespace.Path.def1` and `Some.Namespace.Path.def2` available without the full prefix, so `Some.Namespace.Path.def3` would be unaffected. This works even if `def1` and `def2` are `protected`. * `open Some.Namespace.Path renaming def1 → def1', def2 → def2'` same as `open Some.Namespace.Path (def1 def2)` but `def1`/`def2`'s names are changed to `def1'`/`def2'`. This works even if `def1` and `def2` are `protected`. * `open scoped Some.Namespace.Path1 Some.Namespace.Path2` **only** opens [scoped instances], notations, and attributes from `Namespace1` and `Namespace2`; it does **not** make any other name available. * `open <any of the open shapes above> in` makes the names `open`-ed visible only in the next command or expression. [scoped instance]: https://lean-lang.org/theorem_proving_in_lean4/type_classes.html#scoped-instances (Scoped instances in Theorem Proving in Lean) ## Examples ```lean /-- SKI combinators https://en.wikipedia.org/wiki/SKI_combinator_calculus -/ namespace Combinator.Calculus def I (a : α) : α := a def K (a : α) : β → α := fun _ => a def S (x : α → β → γ) (y : α → β) (z : α) : γ := x z (y z) end Combinator.Calculus section -- open everything under `Combinator.Calculus`, *i.e.* `I`, `K` and `S`, -- until the section ends open Combinator.Calculus theorem SKx_eq_K : S K x = I := rfl end -- open everything under `Combinator.Calculus` only for the next command (the next `theorem`, here) open Combinator.Calculus in theorem SKx_eq_K' : S K x = I := rfl section -- open only `S` and `K` under `Combinator.Calculus` open Combinator.Calculus (S K) theorem SKxy_eq_y : S K x y = y := rfl -- `I` is not in scope, we have to use its full path theorem SKxy_eq_Iy : S K x y = Combinator.Calculus.I y := rfl end section open Combinator.Calculus renaming I → identity, K → konstant #check identity #check konstant end section open Combinator.Calculus hiding S #check I #check K end section namespace Demo inductive MyType | val namespace N1 scoped infix:68 " ≋ " => BEq.beq scoped instance : BEq MyType where beq _ _ := true def Alias := MyType end N1 end Demo -- bring `≋` and the instance in scope, but not `Alias` open scoped Demo.N1 #check Demo.MyType.val == Demo.MyType.val #check Demo.MyType.val ≋ Demo.MyType.val -- #check Alias -- unknown identifier 'Alias' end ``` open コマンドによってスコープに入れられた、識別子の接頭辞と同じグローバル名

識別子が複数の名前に解決される場合は、エラボレータはそれらすべてを使おうとします。そのうち1つだけが成功すればそれが識別子の意味として使用されます。2つ以上成功するか、すべて失敗するとエラーになります。

ローカル名が優先される

ローカル束縛はグローバル束縛よりも優先されます：

def x := "global" "local"#eval let x := "local" x 
"local"

名前の最も内側のローカル束縛が優先されます：

"inner"#eval let x := "outer" let x := "inner" x 
"inner"
より長い現在の名前空間の接頭辞が優先される

名前空間 A ・ B ・ C が入れ子になっており、A と C にはそれぞれ x の定義を含んでいます。

namespace A def x := "A.x" namespace B namespace C def x := "A.B.C.x"

現在の名前空間が A.B.C の場合、 x は A.B.C.x に解決されます。

"A.B.C.x"#eval x 
"A.B.C.x"

現在の名前空間が A.B の場合、 x は A.x に解決されます。

end C "A.x"#eval x 
"A.x"
より長い識別子の接頭辞が優先される

識別子が名前によって異なる射影で参照できる場合、名前が最も長いものが優先されます：

structure A where y : String deriving Repr structure B where y : A deriving Repr def y : B := ⟨⟨"shorter"⟩⟩ def y.y : A := ⟨"longer"⟩

上記の宣言の下、 y.y.y は原則として y の y フィールドの y フィールドを指すことも、 y.y の y フィールドを指すこともできます。これは y.y の y フィールドを指します。なぜなら、y.y.y において y.y は y よりも長い接頭辞になるからです：

"longer"#eval y.y.y 
"longer"
現在の名前空間がオープンされた名前空間よりも優先される

識別子が、現在の名前空間の接頭辞で定義されている名前と、オープンされている名前空間のどちらかを指す可能性がある場合、前者が優先されます。

namespace A def x := "A.x" end A namespace B def x := "B.x" namespace C open A "B.x"#eval x

A は B.x の宣言よりも後にオープンされたにもかかわらず、識別子 x は A.x ではなく B.x に解決されます。なぜなら B は現在の名前空間 B.C の接頭辞であるからです。

"B.x"#eval x 
"B.x"
あいまいな識別子

この例では、x は A.x または B.x のどちらかを指す可能性があり、どちらも優先されません。どちらも同じ型であるため、これはエラーになります。

def A.x := "A.x" def B.x := "B.x" open A open B #eval ambiguous, possible interpretations B.x : String A.x : Stringx 
ambiguous, possible interpretations 
  B.x : String
  
  A.x : String
型付けによるあいまいさの解消

型が異なる場合は、あいまいさをなくすために型が使われます：

def C.x := "C.x" def D.x := 3 open C open D "C.x"#eval (x : String) 
"C.x"

6.1.1. 先頭の（Leading .）

識別子がドット（.）で始まる場合、現在の名前空間や開いている名前空間のセットではなく、エラボレータがその式に期待する型が解決に使用されます。これには 一般化されたフィールド記法 が関連しています：先頭のドット記法は識別子の期待される型を使用して名前に解決しますが、フィールド記法はドットの直前の項の推測される型を使用します。

先頭が . である識別子は 期待された型の名前空間 （expected type's namespace）にて検索されます。ある項に対して期待される型が0個以上の引数に適用される定数である場合、その名前空間はその定数の名前になります。型が定数の適用ではない場合（関数・メタ変数・宇宙等）、名前空間はありません。

その名前が期待される型の名前空間に見つからないが、定数を展開して別の定数を得ることができる場合、その名前空間が参照されます。この処理は定数の適用以外のものに遭遇するか、定数が展開できなくなるまで繰り返されます。

先頭の .

.replicate に期待される型は List Unit です。この型の名前空間は List であるため、 .replicate は List.replicate に解決されます。

[(), (), ()]#eval show List Unit from .replicate 3 () 
[(), (), ()]
先頭の . と定義の展開

.replicate に期待される型は MyList Unit です。この型の名前空間は MyList ですが、MyList.replicate という定義はありません。 MyList Unit を展開すると List Unit が得られるため、 .replicate は List.replicate に解決されます。

def MyList α := List α [(), (), ()]#eval show MyList Unit from .replicate 3 () 
[(), (), ()]