Skip to content
This repository has been archived by the owner on Nov 29, 2024. It is now read-only.

Commit

Permalink
目次の構成を更新
Browse files Browse the repository at this point in the history
  • Loading branch information
Seasawher committed Apr 20, 2024
1 parent 6d3e385 commit a18715a
Showing 1 changed file with 15 additions and 15 deletions.
30 changes: 15 additions & 15 deletions md/SUMMARY.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,25 +4,29 @@

---

# 構文・コマンド
# Lean の構文

* [`_root_`: 一時的に名前空間を抜ける](./build/Root.md)
* [abbrev: 別名を定義する](./build/Abbrev.md)
* [class: 型クラスを定義する](./build/Class.md)
* [def: 関数や項を定義する](./build/Def.md)
* [example: 名前をつけずに証明をする](./build/Example.md)
* [inductive: 帰納型を定義する](./build/Inductive.md)
* [notation: 記法を導入する](./build/Notation.md)
* [protected: フルネームを強制する](./build/Protected.md)
* [structure: 構造体を定義する](./build/Structure.md)
* [theorem: 命題を証明する](./build/Theorem.md)

# 名前空間とセクション

* [`_root_`: 一時的に名前空間を抜ける](./build/Root.md)
* [instance: インスタンスを定義する]()
* [namespace: 定義を階層化する](./build/Namespace.md)
* [open: 名前空間を開く](./build/Open.md)
* [private: 定義を不可視にする]()
* [protected: フルネームを強制する](./build/Protected.md)
* [section: 引数のスコープを区切る](./build/Section.md)
* [structure: 構造体を定義する](./build/Structure.md)
* [theorem: 命題を証明する](./build/Theorem.md)
* [variable: 引数を共通化する](./build/Variable.md)
* [コメント](./build/Comment.md)
* [パイプライン演算子](./build/Pipeline.md)
* [フィールド記法](./build/FieldNotation.md)
* [暗黙の引数]()
* [匿名コンストラクタ](./build/AnonymousConstructor.md)
* [名前付き引数](./build/NamedArgument.md)

# 型クラス

Expand All @@ -32,10 +36,6 @@
* [CoeSort: 型の型強制](./build/CoeSort.md)
* [Inhabited: デフォルトの項を持たせる](./build/Inhabited.md)

# そのほか
# メタプログラミング

* [コメント](./build/Comment.md)
* [フィールド記法](./build/FieldNotation.md)
* [パイプライン演算子](./build/Pipeline.md)
* [匿名コンストラクタ](./build/AnonymousConstructor.md)
* [名前付き引数](./build/NamedArgument.md)
* [notation: 記法を導入する](./build/Notation.md)

0 comments on commit a18715a

Please sign in to comment.