3.1. ファイル（Files）🔗

Lean におけるコンパイルの最小単位は1つの モジュール （module）です。モジュールはソースファイルに対応し、ファイル名に基づいて他のモジュールにインポートされます。言い換えれば、Lean コードではファイルの名前とフォルダ構造が重要です。

3.1.1. モジュール（Modules）🔗

すべての Lean ファイルはモジュールを定義します。モジュールの名前はファイル名と Lean の起動方法の組み合わせで決まります：Lean はコードを見つけることを期待する ルートディレクトリ （root directory）を持っており、モジュールの名前はルートからファイル名までのディレクトリの名前にドット（.）を散りばめ、.lean を取り除いたものです。例えば、Lean が Projects/MyLib/src をルートとして起動された場合、Projects/MyLib/src/Literature/Novel/SciFi.lean というファイルには Literature.Novel.SciFi という名前のモジュールが含まれます。

3.1.1.1. エンコードと表現（Encoding and Representation）🔗

Lean モジュールは UTF-8 でエンコードされた Unicode テキストファイルです。行の終わりは改行文字（"\n"、Unicode 'LINE FEED (LF)' (U+000A)）か、改ページと改行の連なり（"\r\n"、Unicode 'CARRIAGE RETURN (CR)' (U+000D) followed by 'LINE FEED (LF)' (U+000A)）のどちらかです。しかし、Lean はファイルを解析したり比較したりするときに行末を正規化するため、すべてのファイルはあたかもすべての行末が "\n" であるかのように比較されます。

3.1.1.2. 具体的な構文（Concrete Syntax）🔗

Lean の具体的な構文は拡張可能です。Lean のような言語では、新しい定数やデータ型に加えて、ライブラリが構文を定義する可能性があるため、構文を完全に記述することはできません。ここでは言語を完全に説明するのではなく、全体的な枠組みを説明し、言語を構成するそれぞれの構文は、それが属する節で説明します。

3.1.1.2.1. 空白（Whitespace）🔗

Lean における字句は 空白 （whitespace）文字の列でいくつでも区切ることができます。空白はスペース（" "、Unicode 'SPACE (SP)' (U+0020)）・有効な改行の列・もしくはコメントです。タブ文字と改行が続かない CR はどちらも有効な空白列ではありません。

3.1.1.2.2. コメント（Comments）🔗

コメントは空白でないにもかかわらず、そのように扱われるのはファイルの伸縮性です。Lean には2つのコメントについての構文があります：

行コメント

字句の一部として出現しない -- は 行コメント を開始します。最初の - から改行までのすべての文字は空白として扱われます。

ブロックコメント

直後に - が続かず、字句の一部として出現しない /- は ブロックコメント を開始します。 /-- はコメントではなくドキュメント文字列を開始します。

3.1.1.2.3. キーワードと識別子（Keywords and Identifiers）🔗

identifier は '.' 区切りで1つ以上の識別子要素から構成されます。

識別子要素 （Identifier component）は、文字・文字様文字・アンダースコア（'_'）とそれに続く0個以上の識別子継続文字から構築されます。文字は大文字または小文字の英語アルファベット、文字様文字には Lean で広く使用されているギリシャ文字や重ね打ち体（ℕ や ℤ を含む）や省略形を含む Unicode の文字様記号ブロックの要素など英語以外のアルファベット文字が含まれます。識別子継続文字は文字・文字様文字・アンダースコア（'_'）・感嘆符（'!'）・疑問符（'?'）・下付き文字・シングルクォート（'）から構成されます。例外として、アンダースコアのみは有効な識別子ではありません。

識別子要素は二重ギュメ（'«' と '»'）で囲むこともできます。このような識別子要素には '»' 以外であれば '«' や改行文字でさえも含めたどのような文字でも含めることができます。

識別子要素として予約キーワードを使うことがあるかもしれません。予約キーワードの特定のセットは、アクティブな構文拡張のセットに依存し、またそれらはインポートされたモジュールと現在開いている名前空間のセットに依存するかもしれません；Lean はこれを列挙することができません。これらのキーワードはほとんどの構文で識別子の構成要素として使用するために、ギュメでクォートする必要があります。帰納型のコンストラクタ名など、キーワードをギュメなしで識別子として使用できるコンテキストは 生識別子 （raw identifier）コンテキストです。

1つ以上の '.' 文字を含み、複数の識別子要素から構成される識別子を 階層的識別子 （hierarchical identifier）と呼ばれます。階層的識別子はモジュールの名前と名前空間の名前の両方を表現するために用いられます。

3.1.1.3. 構造体（Structure）🔗

syntax
Parser for a Lean module. We never actually run this parser but instead use the imperative definitions below that
return the same syntax tree structure, but add error recovery. Still, it is helpful to have a `Parser` definition
for it in order to auto-generate helpers such as the pretty printer. module ::=
    Parser for a Lean module. We never actually run this parser but instead use the imperative definitions below that
return the same syntax tree structure, but add error recovery. Still, it is helpful to have a `Parser` definition
for it in order to auto-generate helpers such as the pretty printer. header command*

モジュールは モジュールヘッダ （module header）とそれに続く コマンド （command）の列から構成されます。

3.1.1.3.1. モジュールヘッダ（Module Headers）🔗

モジュールヘッダは import 文 の列から構成されます。

syntax
header ::=
    import*

Lean の実装で使用するために、オプションのキーワードとして prelude も使用することができます：

header ::= ...
    | prelude import*
syntax
prelude ::=
    prelude

prelude キーワードは、そのモジュールが Lean の prelude の実装の一部となることを示しています。prelude は明示的にモジュールのインポートをしなくても利用可能なコードです。このキーワードは Lean の実装外では使うべきではありません。

syntax
import ::= ...
    | import ident

モジュールのインポートについて。モジュールのインポートによってその内容を現在のモジュールで利用できるようになり、またそのインポート先がインポートしているモジュールからも遷移的に利用可能です。

モジュールは必ずしも名前空間に対応するとは限りません。モジュールはどの名前空間にも名前を追加することができ、モジュールをインポートしても現在開いている名前空間のセットには影響しません。

インポートされたモジュール名は、その名前のドット（'.'）をディレクトリの区切り文字に置き換えることでファイル名に変換されます。Lean は対応するインポート可能なモジュールファイルをインクルードパスから検索します。

3.1.1.3.2. コマンド（Commands）🔗

コマンド （command）は Lean においてトップレベルの文です。例えば、帰納型の宣言・定理・関数定義・open や variable などの名前空間修飾子・#check のような対話的クエリなどです。コマンドの構文はユーザが拡張可能です。特定の Lean コマンドについてはここに列挙するのではなく、このマニュアルの対応する章で説明しています。

3.1.1.4. 内容（Contents）🔗

モジュールには環境が含まれます。これには環境からの帰納型と定数定義、環境拡張に格納されたデータの両方が含まれます。Lean によってモジュールが処理されると、コマンドは環境に内容を追加します。モジュールの環境は .olean ファイル にシリアライズすることができ、これには環境と環境によって必要とされるランタイムオブジェクトを含むコンパクト化されたヒープ領域の両方を含みます。これはインポートされたモジュールが、そのコマンドをすべて再実行することなくロードできることを意味します。

3.1.2. パッケージ・ライブラリ・ターゲット（Packages, Libraries, and Targets）🔗

Lean のコードはコード配布の単位である パッケージ （package）へと編成されます。 パッケージ には複数のライブラリや実行ファイルが含まれることがあります。

他の Lean パッケージで使用することを意図したパッケージ内のコードは ライブラリ に編成されます。独立したプログラムとしてコンパイルされ実行されることを意図したコードは 実行ファイル に編成されます。Lean の標準的なビルドツールである Lake では、ライブラリと実行ファイルを合わせて ターゲット と呼んでいます。