Skip to content
This repository was archived by the owner on Jan 5, 2025. It is now read-only.

Commit ef96af3

Browse files
committed
誤字修正
1 parent 04e25d1 commit ef96af3

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

Manual/Elaboration.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -82,7 +82,7 @@ Roughly speaking, Lean's processing of a source file can be divided into the fol
8282

8383
: エラボレーション
8484

85-
{deftech key:="エラボレータ"}[エラボレーション] (elaboration)とは、Lean のユーザ向けの構文をコア型理論に変換するプロセスです。このコア理論はよりシンプルであり、信頼されたカーネルを非常に小さくすることができます。エラボレーションはさらに、Lean の対話的帰納に使用される証明状態や式の型などのメタデータを生成し、サイドテーブルに格納します。
85+
{deftech key:="エラボレータ"}[エラボレーション] (elaboration)とは、Lean のユーザ向けの構文をコア型理論に変換するプロセスです。このコア理論はよりシンプルであり、信頼されたカーネルを非常に小さくすることができます。エラボレーションはさらに、Lean の対話的機能に使用される証明状態や式の型などのメタデータを生成し、サイドテーブルに格納します。
8686

8787
:::comment
8888
: Kernel Checking

0 commit comments

Comments
 (0)