diff --git a/GLOSSARY.md b/GLOSSARY.md index 6126350..f55f355 100644 --- a/GLOSSARY.md +++ b/GLOSSARY.md @@ -2,12 +2,14 @@ | 英語 | 日本語 | 備考 | | --- | --- | --- | +| abbreviation | 省略形 | | | annotation | 注釈 | | | associativity | 結合性 | | | attribute | 属性 | | | backtrack | バックトラック | 後戻りと書かれる場合あり | | bound variable | 束縛変数 | | | canonical | 標準 | | +| carriage return | CR | | | case distinction | 場合分け | | | chapter | 章 | | | closed term | 閉項 | | @@ -20,6 +22,8 @@ | constant | 定数 | | | construction | 構成 | | | constructor | コンストラクタ | | +| content | 内容 | | +| context | （プログラム中のcontextの意で）コンテキスト、（文章中のcontextの意で）文脈 | | | core language | コア言語 | | | core type theory | コア型理論 | | | datatype | データ型 | | @@ -29,22 +33,32 @@ | definitional (η-)equality | 定義上の(η)等価性 | | | definitional proof irrelevance | 定義上の証明の無関係性 | | | dependent type theory | 依存型理論 | | +| double-struck | 重ね打ち体 | | | effect | 作用 | | | elaborate | エラボレート | | | elaboration | エラボレーション | | | elaborator | エラボレータ | | +| encoding | エンコード | | +| English letter | 英語アルファベット | | | environment | 環境 | | | environment extensions | 環境拡張 | | | equational lemma | 等式の補題 | | | evaluate | 評価 | | +| exclamation mark | 感嘆符 | | | executable | 実行ファイル | | | expression | 式 | | | formalization | 形式化 | | +| form feed | 改ページ | | | functional programming language | 関数型プログラミング言語 | | | function extensionality | 関数外延性 | | | grammar | 文法 | | +| guillemet | ギュメ | フランス語 | +| heap region | ヒープ領域 | | +| hierarchical identifier | 階層的識別子 | | | hierarchy | 階層 | | | identifier | 識別子 | | +| identifier component | 識別子要素 | | +| identifier continuation character | 識別子継続文字 | | | inductively-defined | 帰納的に定義された | | | inductive predicate | 帰納的述語 | | | inductive type | 帰納型 | | @@ -61,6 +75,8 @@ | laziness | 遅延 | | | language server | 言語サーバ | | | lemma | 補題 | | +| letter | 文字 | | +| letterlike | 文字様 | | | longest match | 最長一致 | | | macro | マクロ | | | machinery | 機構 | | @@ -71,6 +87,7 @@ | multi-threading | マルチスレッド | | | mutually inductive | 相互帰納 | | | namespace | 名前空間 | | +| newline | 改行 | | | notation | 記法 | | | opaque | 不透明 | | | operator | 演算子 | | @@ -86,23 +103,34 @@ | proof state | 証明状態 | | | proof term | 証明項 | | | qualification | 修飾 | | +| question mark | 疑問符 | | +| quote | クォート | | | quotient type | 商型 | | +| raw identifier | 生識別子 | Rust By Exampleの表現を利用 | | reasoning | 推論 | | | recovery | 回復 | | | recursive-descent parser | 再帰下降パーサ | | | reference count | 参照カウント | +| representation | 表現 | | +| reserved keyword | 予約キーワード | 下のreserved wordの表記ゆれかもしれないがいったん別の訳語を割り当てる | | reserved word | 予約語 | | | run-time | ランタイム | | | rule | ランタイム | | | scope | スコープ | | +| separator | 区切り文字 | | | set | （数学的な集合を意味しない場合）あつまり、（数学的な集合の場合）集合 | | | section | 節 | | +| serialize | シリアライズ | | | side effect | 副作用 | | | signature | シグネチャ | | +| single quote | シングルクォート | | | soundness | 健全性 | | | specialization | 特殊化 | | +| statement | 文 | | | strictness | 正格 | | +| structure | 構造体 | | | subterm | 部分項 | | +| subscript | 下付き文字 | | | syntactic sugar | 構文糖衣 | | | syntax | 構文 | | | syntax former | 構文形成器 | | @@ -114,6 +142,7 @@ | term | 項 | | | term elaboration | 項エラボレーション | | | termination | 停止 | | +| theorem | 定理 | | | token | 字句 | | | top-level | トップレベル | | | transitive | 推移的 | | @@ -122,10 +151,11 @@ | trust | 信頼 | | | type class | 型クラス | | | type class instance synthesis | 型クラスインスタンス合成 | | +| underscore | アンダースコア | | | unification | 単一化 | | | union | 合併 | | | well-founded | 整礎 | | -| whitespace | 空白文字 | | +| whitespace | 空白 | | # 英語表現をそのまま用いている単語 @@ -134,4 +164,5 @@ | --- | --- | | choice node | | | packed array | System Verilogという言語にこの名前の文法要素がある？ | +| prelude | | | subject reduction | TAPLに出てくる模様 | \ No newline at end of file diff --git a/Manual/Elaboration.lean b/Manual/Elaboration.lean index 353d1da..67df3b4 100644 --- a/Manual/Elaboration.lean +++ b/Manual/Elaboration.lean @@ -118,7 +118,7 @@ There are multiple kinds of elaboration: command elaboration implements the effe Tactic execution is a specialization of term elaboration. ::: -実際には、上記の段階は厳密に次々と行われるわけではありません。Lean は1つの {tech}[command] （トップレベルの宣言）をパースし、ついでエラボレートし、必要なカーネルのチェックを実行します。マクロ展開はエラボレーションの一部です；構文の一部を翻訳する前に、エラボレータはまず一番外側のレイヤに存在するマクロを展開します。マクロ構文はより深いレイヤに残っているかもしれませんが、その後でエラボレータがそれらのレイヤに到達した時に展開されます。エラボレーションには複数の種類が存在します：コマンドエラボレーションは各トップレベルのコマンドの作用（例えばデータ型の宣言・定義の保存・式の評価）を実装し、項エラボレーションは多くのコマンドで出現する項（例えばシグネチャ内の型・定義の右辺・評価される式）の構築を担当します。タクティクの実行は、項エラボレーションの特殊化です。 +実際には、上記の段階は厳密に次々と行われるわけではありません。Lean は1つの {tech}[コマンド] （command、トップレベルの宣言）をパースし、ついでエラボレートし、必要なカーネルのチェックを実行します。マクロ展開はエラボレーションの一部です；構文の一部を翻訳する前に、エラボレータはまず一番外側のレイヤに存在するマクロを展開します。マクロ構文はより深いレイヤに残っているかもしれませんが、その後でエラボレータがそれらのレイヤに到達した時に展開されます。エラボレーションには複数の種類が存在します：コマンドエラボレーションは各トップレベルのコマンドの作用（例えばデータ型の宣言・定義の保存・式の評価）を実装し、項エラボレーションは多くのコマンドで出現する項（例えばシグネチャ内の型・定義の右辺・評価される式）の構築を担当します。タクティクの実行は、項エラボレーションの特殊化です。 :::comment When a command is elaborated, the state of Lean changes. @@ -161,9 +161,9 @@ Based on the {lean}`SourceInfo` field, there are three relationships that {lean} * {lean}`SourceInfo.none` indicates no relationship to a file. ::: -成功した場合、パーサは元のソースファイルを再構築するのに十分な情報を保存します。成功しなかったパースは、パース出来なかったファイルの領域に関する情報を見逃す可能性があります。 {lean}`SourceInfo` レコード型はソースの位置と周囲の空白文字を含む、構文の一部分のソースに関する情報を記録します。 {lean}`SourceInfo` フィールドに基づいて、 {lean}`Syntax` がソースファイルに対して以下の3つの関係を持つことができます： +成功した場合、パーサは元のソースファイルを再構築するのに十分な情報を保存します。成功しなかったパースは、パース出来なかったファイルの領域に関する情報を見逃す可能性があります。 {lean}`SourceInfo` レコード型はソースの位置と周囲の空白を含む、構文の一部分のソースに関する情報を記録します。 {lean}`SourceInfo` フィールドに基づいて、 {lean}`Syntax` がソースファイルに対して以下の3つの関係を持つことができます： * {lean}`SourceInfo.original` は、構文の値がパーサによって直接生成されたことを示します。 - * {lean}`SourceInfo.synthetic` は、構文の値がマクロ展開などによってプログラム的に生成されたことを示します。そうであるにも関わらず、統合的な構文は _標準_ （canonical）とマークされることがあります。これによって Lean のユーザインタフェースはこの構文をあたかもユーザが書いたかのように扱います。統合的な構文には元のファイル位置が注釈されますが、先頭や末尾の空白文字は含まれません。 + * {lean}`SourceInfo.synthetic` は、構文の値がマクロ展開などによってプログラム的に生成されたことを示します。そうであるにも関わらず、統合的な構文は _標準_ （canonical）とマークされることがあります。これによって Lean のユーザインタフェースはこの構文をあたかもユーザが書いたかのように扱います。統合的な構文には元のファイル位置が注釈されますが、先頭や末尾の空白は含まれません。 * {lean}`SourceInfo.none` は、ファイルとの関係がないことを示します。 :::comment diff --git a/Manual/Language/Files.lean b/Manual/Language/Files.lean index eafe70f..24e988d 100644 --- a/Manual/Language/Files.lean +++ b/Manual/Language/Files.lean @@ -10,64 +10,136 @@ import Manual.Meta open Verso.Genre Manual +/- #doc (Manual) "Files" => +-/ +#doc (Manual) "ファイル" => +:::comment The smallest unit of compilation in Lean is a single {deftech}[module]. Modules correspond to source files, and are imported into other modules based on their filenames. In other words, the names and folder structures of files are significant in Lean code. +::: +Lean におけるコンパイルの最小単位は1つの {deftech}[モジュール] （module）です。モジュールはソースファイルに対応し、ファイル名に基づいて他のモジュールにインポートされます。言い換えれば、Lean コードではファイルの名前とフォルダ構造が重要です。 + +:::comment # Modules +::: +# モジュール + +:::comment Every Lean file defines a module. A module's name is derived from a combination of its filename and the way in which Lean was invoked: Lean has a _root directory_ in which it expects to find code, and the module's name is the names of the directories from the root to the filename, with dots (`.`) interspersed and `.lean` removed. For example, if Lean is invoked with `Projects/MyLib/src` as its root, the file `Projects/MyLib/src/Literature/Novel/SciFi.lean` would contain a module named `Literature.Novel.SciFi`. +::: + +すべての Lean ファイルはモジュールを定義します。モジュールの名前はファイル名と Lean の起動方法の組み合わせで決まります：Lean はコードを見つけることを期待する _ルートディレクトリ_ （root directory）を持っており、モジュールの名前はルートからファイル名までのディレクトリの名前にドット（`.`）を散りばめ、`.lean` を取り除いたものです。例えば、Lean が `Projects/MyLib/src` をルートとして起動された場合、`Projects/MyLib/src/Literature/Novel/SciFi.lean` というファイルには `Literature.Novel.SciFi` という名前のモジュールが含まれます。 ::: TODO Describe case sensitivity/preservation for filenames here ::: +:::comment ## Encoding and Representation +::: + +## エンコードと表現 +:::comment Lean modules are Unicode text files encoded in UTF-8. {TODO}[Figure out the status of BOM and Lean] Lines may end either with newline characters (`"\n"`, Unicode `'LINE FEED (LF)' (U+000A)`) or with a form feed and newline sequence (`"\r\n"`, Unicode `'CARRIAGE RETURN (CR)' (U+000D)` followed by `'LINE FEED (LF)' (U+000A)`). However, Lean normalizes line endings when parsing or comparing files, so all files are compared as if all their line endings are `"\n"`. +::: + +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"` であるかのように比較されます。 + ::: TODO Marginal note: this is to make cached files and `#guard_msgs` and the like work even when git changes line endings. Also keeps offsets stored in parsed syntax objects consistent. ::: +:::comment ## Concrete Syntax +::: + +## 具体的な構文 +:::comment Lean's concrete syntax is extensible. In a language like Lean, it's not possible to completely describe the syntax once and for all, because libraries may define syntax in addition to new constants or datatypes. Rather than completely describing the language here, the overall framework is described, while the syntax of each language construct is documented in the section to which it belongs. +::: + +Lean の具体的な構文は拡張可能です。Lean のような言語では、新しい定数やデータ型に加えて、ライブラリが構文を定義する可能性があるため、構文を完全に記述することはできません。ここでは言語を完全に説明するのではなく、全体的な枠組みを説明し、言語を構成するそれぞれの構文は、それが属する節で説明します。 +:::comment ### Whitespace +::: + +### 空白 +:::comment Tokens in Lean may be separated by any number of {deftech}[_whitespace_] character sequences. Whitespace may be a space (`" "`, Unicode `'SPACE (SP)' (U+0020)`), a valid newline sequence, or a comment. {TODO}[xref] Neither tab characters nor carriage returns not followed by newlines are valid whitespace sequences. +::: + +Lean における字句は {deftech}[_空白_] （whitespace）文字の列でいくつでも区切ることができます。空白はスペース（`" "`、Unicode `'SPACE (SP)' (U+0020)`）・有効な改行の列・もしくはコメントです。タブ文字と改行が続かない CR はどちらも有効な空白列ではありません。 +:::comment ### Comments +::: +### コメント + +:::comment Comments are stretches of the file that, despite not being whitespace, are treated as such. Lean has two syntaxes for comments: +::: +コメントは空白でないにもかかわらず、そのように扱われるのはファイルの伸縮性です。Lean には2つのコメントについての構文があります： + +:::comment : Line comments A `--` that does not occur as part of a token begins a _line comment_. All characters from the initial `-` to the newline are treated as whitespace.{index (subterm := "line")}[comment] +::: + +: 行コメント + 字句の一部として出現しない `--` は _行コメント_ を開始します。最初の `-` から改行までのすべての文字は空白として扱われます。 {index (subterm := "line")}[comment] + +:::comment : Block comments A `/-` that does not occur as part of a token and is not immediately followed by a `-` character begins a _block comment_.{index (subterm := "block")}[comment] `/--` begins a documentation string {TODO}[xref] rather than a comment. +::: +: ブロックコメント + + 直後に `-` が続かず、字句の一部として出現しない `/-` は _ブロックコメント_ を開始します。 {index (subterm := "block")}[comment] `/--` はコメントではなくドキュメント文字列を開始します。 + +:::comment ### Keywords and Identifiers +::: +### キーワードと識別子 + +:::comment An {deftech}[identifier] consists of one or more identifier components, separated by `'.'`.{index}[identifier] +::: +{deftech}[識別子] （identifier）は `'.'` 区切りで1つ以上の識別子要素から構成されます。 {index}[identifier] + +:::comment {deftech}[Identifier components] consist of a letter or letterlike character or an underscore (`'_'`), followed by zero or more identifier continuation characters. Letters are English letters, upper- or lowercase, and the letterlike characters include a range of non-English alphabetic scripts, including the Greek script which is widely used in Lean, as well as the members of the Unicode letterlike symbol block, which contains a number of double-struck characters (including `ℕ` and `ℤ`) and abbreviations. Identifier continuation characters consist of letters, letterlike characters, underscore (`'_'`), exclamation mark (`!`), question mark (`?`), subscripts, and single quotes (`'`). As an exception, underscore alone is not a valid identifier. +::: + +{deftech}[識別子要素] （Identifier component）は、文字・文字様文字・アンダースコア（`'_'`）とそれに続く0個以上の識別子継続文字から構築されます。文字は大文字または小文字の英語アルファベット、文字様文字には Lean で広く使用されているギリシャ文字や重ね打ち体（`ℕ` や `ℤ` を含む）や省略形を含む Unicode の文字様記号ブロックの要素など英語以外のアルファベット文字が含まれます。識別子継続文字は文字・文字様文字・アンダースコア（`'_'`）・感嘆符（`'!'`）・疑問符（`'?'`）・下付き文字・シングルクォート（`'`）から構成されます。例外として、アンダースコアのみは有効な識別子ではありません。 ````lean (show := false) def validIdentifier (str : String) : IO String := @@ -122,8 +194,12 @@ def validIdentifier (str : String) : IO String := ```` +:::comment Identifiers components may also be surrounded by double guillemets (`'«'` and `'»'`). Such identifier components may contain any character at all, aside from `'»'`, even `'«'` and newlines. +::: + +識別子要素は二重ギュメ（`'«'` と `'»'`）で囲むこともできます。このような識別子要素には `'»'` 以外であれば `'«'` や改行文字でさえも含めたどのような文字でも含めることができます。 ```lean (show := false) /-- info: "Success! Final stack:\n `«\n »\nAll input consumed." -/ @@ -135,97 +211,168 @@ Such identifier components may contain any character at all, aside from `'»'`, #eval validIdentifier "««one line\nand another»" ``` +:::comment Some potential identifier components may be reserved keywords. The specific set of reserved keywords depends on the set of active syntax extensions, which may depend on the set of imported modules and the currently-opened {TODO}[xref/deftech for namespace] namespaces; it is impossible to enumerate for Lean as a whole. These keywords must also be quoted with guillemets to be used as identifier components in most syntactic contexts. Contexts in which keywords may be used as identifiers without guillemets, such as constructor names in inductive datatypes, are {deftech}_raw identifier_ contexts.{index (subterm:="raw")}[identifier] +::: + +識別子要素として予約キーワードを使うことがあるかもしれません。予約キーワードの特定のあつまりは、アクティブな構文拡張のあつまりに依存し、またそれらはインポートされたモジュールと現在開いている名前空間のあつまりに依存するかもしれません；Lean はこれを列挙することができません。これらのキーワードはほとんどの構文で識別子の構成要素として使用するために、ギュメでクォートする必要があります。帰納的データ型のコンストラクタ名など、キーワードをギュメなしで識別子として使用できるコンテキストは {deftech}_生識別子_ （raw identifier）コンテキストです。 {index (subterm:="raw")}[identifier] +:::comment Identifiers that contain one or more `'.'` characters, and thus consist of more than one identifier component, are called {deftech}[hierarchical identifiers]. Hierarchical identifiers are used to represent both module names and names in a namespace. +::: + +1つ以上の `'.'` 文字を含み、複数の識別子要素から構成される識別子を {deftech}[階層的識別子] （hierarchical identifier）と呼ばれます。階層的識別子はモジュールの名前と名前空間の名前の両方を表現するために用いられます。 +:::comment ## Structure +::: + +## 構造体 %%% tag := "module-structure" %%% - -:::syntax Lean.Parser.Module.module (open := false) +::::syntax Lean.Parser.Module.module (open := false) ```grammar $hdr:header $cmd:command* ``` +:::comment A module consists of a {deftech}_module header_ followed by a sequence of {deftech}_commands_. - ::: +モジュールは {deftech}_モジュールヘッダ_ （module header）とそれに続く {deftech}_コマンド_ （command）の列から構成されます。 + +:::: +:::comment ### Module Headers +::: + +### モジュールヘッダ +:::comment The module header consists of a sequence of {deftech}[`import` statements]. +::: -:::syntax Lean.Parser.Module.header (open := false) +モジュールヘッダは {deftech}[`import` 文] の列から構成されます。 + +::::syntax Lean.Parser.Module.header (open := false) ```grammar $i:import* ``` +:::comment An optional keyword `prelude`, for use in Lean's implementation, is also allowed: +::: + +Lean の実装で使用するために、オプションのキーワードとして `prelude` も使用することができます： ```grammar prelude $«import»* ``` -::: +:::: -:::syntax Lean.Parser.Module.prelude (open := false) +::::syntax Lean.Parser.Module.prelude (open := false) ```grammar prelude ``` +:::comment The `prelude` keyword indicates that the module is part of the implementation of the Lean {deftech}_prelude_, which is the code that is available without explicitly importing any modules—it should not be used outside of Lean's implementation. ::: -:::syntax Lean.Parser.Module.import +`prelude` キーワードは、そのモジュールが Lean の {deftech}_prelude_ の実装の一部となることを示しています。prelude は明示的にモジュールのインポートをしなくても利用可能なコードです。このキーワードは Lean の実装外では使うべきではありません。 + +:::: + +::::syntax Lean.Parser.Module.import ```grammar import $mod:ident ``` +:::comment Imports the module. Importing a module makes its contents available in the current module, as well as those from modules transitively imported by its imports. +::: + +モジュールのインポートについて。モジュールのインポートによってその内容を現在のモジュールで利用できるようになり、またそのインポート先がインポートしているモジュールからも遷移的に利用可能です。 +:::comment Modules do not necessarily correspond to namespaces. Modules may add names to any namespace, and importing a module has no effect on the set of currently open namespaces. +::: +モジュールは必ずしも名前空間に対応するとは限りません。モジュールはどの名前空間にも名前を追加することができ、モジュールをインポートしても現在開いている名前空間のあつまりには影響しません。 + +:::comment The imported module name is translated to a filename by replacing dots (`'.'`) in its name with directory separators. Lean searches its include path for the corresponding importable module file. ::: +インポートされたモジュール名は、その名前のドット（`'.'`）をディレクトリの区切り文字に置き換えることでファイル名に変換されます。Lean は対応するインポート可能なモジュールファイルをインクルードパスから検索します。 + +:::: + +:::comment ### Commands +::: + +### コマンド +:::comment {tech}[Commands] are top-level statements in Lean. Some examples are inductive type declarations, theorems, function definitions, namespace modifiers like `open` or `variable`, and interactive queries such as `#check`. The syntax of commands is user-extensible. Specific Lean commands are documented in the corresponding chapters of this manual, rather than being listed here. +::: + +{tech}[コマンド] （command）は Lean においてトップレベルの文です。例えば、帰納型の宣言・定理・関数定義・`open` や `variable` などの名前空間修飾子・`#check` のような対話的クエリなどです。コマンドの構文はユーザが拡張可能です。特定の Lean コマンドについてはここに列挙するのではなく、このマニュアルの対応する章で説明しています。 ::: TODO Make the index include links to all commands, then xref from here ::: +:::comment ## Contents +::: + +## 内容 +:::comment A module includes an {TODO}[def and xref] environment, which includes both the datatype and constant definitions from an environment and any data stored in {TODO}[xref] its environment extensions. As the module is processed by Lean, commands add content to the environment. A module's environment can be serialized to a {deftech (key:="olean")}[`.olean` file], which contains both the environment and a compacted heap region with the run-time objects needed by the environment. This means that an imported module can be loaded without re-executing all of its commands. +::: +モジュールには環境が含まれます。これには環境からのデータ型と定数定義、環境拡張に格納されたデータの両方が含まれます。Lean によってモジュールが処理されると、コマンドは環境に内容を追加します。モジュールの環境は {deftech (key:="olean")}[`.olean` ファイル] にシリアライズすることができ、これには環境と環境によって必要とされるランタイムオブジェクトを含むコンパクト化されたヒープ領域の両方を含みます。これはインポートされたモジュールが、そのコマンドをすべて再実行することなくロードできることを意味します。 +:::comment # Packages, Libraries, and Targets +::: + +# パッケージ・ライブラリ・ターゲット +:::comment Lean code is organized into {deftech}_packages_, which are units of code distribution. A {tech}[package] may contain multiple libraries or executables. +::: + +Lean のコードはコード配布の単位である {deftech}_パッケージ_ （package）へと編成されます。 {tech}[パッケージ] には複数のライブラリや実行ファイルが含まれることがあります。 +:::comment Code in a package that is intended for use by other Lean packages is organized into {deftech (key:="library")}[libraries]. Code that is intended to be compiled and run as independent programs is organized into {deftech (key:="executable")}[executables]. Together, libraries and executables are referred to as {deftech}_targets_ in Lake, the standard Lean build tool. {TODO}[section xref] +::: + +他の Lean パッケージで使用することを意図したパッケージ内のコードは {deftech (key:="library")}[ライブラリ] に編成されます。独立したプログラムとしてコンパイルされ実行されることを意図したコードは {deftech (key:="executable")}[実行ファイル] に編成されます。Lean の標準的なビルドツールである Lake では、ライブラリと実行ファイルを合わせて {deftech}_ターゲット_ と呼んでいます。 :::TODO Write Lake section, coordinate this content with it diff --git a/Manual/Language/InductiveTypes.lean b/Manual/Language/InductiveTypes.lean index a029284..61b46f7 100644 --- a/Manual/Language/InductiveTypes.lean +++ b/Manual/Language/InductiveTypes.lean @@ -62,7 +62,7 @@ In some situations, this process may fail to find a minimal universe or fail to The constructor specifications follow {keywordOf Lean.Parser.Command.declaration (parser:=«inductive»)}`where`. Constructors are not mandatory, as constructorless datatypes such as {lean}`False` and {lean}`Empty` are perfectly sensible. Each constructor specification begins with a vertical bar (`'|'`, Unicode `'VERTICAL BAR' (U+007c)`), declaration modifiers, and a name. -The name is a {tech}[raw identifier]. +The name is a {tech}[生識別子]raw identifier. A declaration signature follows the name. The signature may specify any parameters, modulo the well-formedness requirements for inductive type declarations, but the return type in the signature must be a saturated application of the type constructor of the inductive type being specified. If no signature is provided, then the constructor's type is inferred by inserting sufficient implicit parameters to construct a well-formed return type.