Skip to content

帰納型の冒頭の説明がわかりづらい #1507

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Feb 6, 2025
Merged

帰納型の冒頭の説明がわかりづらい #1507

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions LeanByExample/Declarative/Inductive.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
/- # inductive
`inductive` コマンドは、帰納型(inductive type)を定義することができます。
`inductive` コマンドは、**帰納型(inductive type)** を定義することができます。

帰納型とは、有限個のコンストラクタで構成され、すべての項がいずれかのコンストラクタで構成されることやコンストラクタの像が重ならないことなど、帰納的構成が満たすべきルールが保証されているような型のことです。
帰納型とは、Lean においてユーザが新しい型を定義するための主要な方法です。帰納型はその型の項を得るための有限個の関数（コンストラクタ）を組み合わせることによって定まります。コンストラクタがこれから定義しようとしている型自身を引数に含むことも許されるので、帰納型は再帰的な構造を持つことができます。

## 帰納型の例

Expand Down