名前

カーネルのプリミティブ型の中でも最初のものは Name で、これはその名称の通りのもののあつまりを指します；これはアドレスのための方法を備えたカーネルの要素を提供します。

Name ::= anonymous | str Name String | num Name Nat

Name 型の要素はドット区切りの名前で表示されます。これはおそらく Lean ユーザにはなじみ深いでしょう。例えば、num (str (anonymous) "foo") 7 は foo.7 と表示されます。

実装についての注記

名前の実装では、文字が Unicode scalar である UTF-8 文字列を想定しています（言語の文字列型のこの実装に関するこれらの想定は、文字列リテラルのカーネル拡張にとっても重要です）。

名前の字句構造に関するいくつかの情報については こちら を参照してください。

エクスポータは匿名の名前を明示的に出力せず、インポートされた名前の0番目の要素であることを期待します。