Skip to content
This repository was archived by the owner on Jan 5, 2025. It is now read-only.
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
1 change: 1 addition & 0 deletions .vale/styles/config/ignore/names.txt
Original file line number Diff line number Diff line change
Expand Up @@ -10,3 +10,4 @@ Selsam
Simons
Ullrich
Wadler
Zulip
1 change: 1 addition & 0 deletions GLOSSARY.md
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,7 @@
| command elaboration | コマンドエラボレーション | |
| compilation | コンパイル | |
| completion | 補完 | |
| configuration item | 設定項目 | |
| confluence | 合流性 | |
| conjunction | 連言 | |
| consistency | 一貫性 | |
Expand Down
2 changes: 1 addition & 1 deletion Manual.lean
Original file line number Diff line number Diff line change
Expand Up @@ -168,7 +168,7 @@ file := some "the-index"

翻訳に際して、機械翻訳サービス [DeepL翻訳](https://www.deepl.com/ja/translator) を参考にしました。

この翻訳は原文のcommit [2fbf58d9210323e4ebc0a002d9f761074da462cf](https://github.com/leanprover/reference-manual/commit/2fbf58d9210323e4ebc0a002d9f761074da462cf) に基づいています。
この翻訳は原文のcommit [ade9c553a5ab008113cf33f88ced657c5146fe24](https://github.com/leanprover/reference-manual/commit/ade9c553a5ab008113cf33f88ced657c5146fe24) に基づいています。

::::::draft

Expand Down
36 changes: 18 additions & 18 deletions Manual/BasicTypes.lean
Original file line number Diff line number Diff line change
Expand Up @@ -85,47 +85,47 @@ tag := "Float"

:::comment
# Characters
:::

# 文字(Characters)
%%%
tag := "Char"
%%%


:::

# 文字(Characters)

{docstring Char}

:::comment
## Syntax
:::

## 構文(Syntax)
%%%
tag := "char-syntax"
%%%


:::

## 構文(Syntax)

:::comment
## Logical Model
:::

## 論理モデル(Logical Model)
%%%
tag := "char-model"
%%%

:::

## 論理モデル(Logical Model)

:::comment
## Run-Time Representation
:::

## ランタイム表現(Run-Time Representation)
%%%
tag := "char-runtime"
%%%

:::

## ランタイム表現(Run-Time Representation)

:::comment
In monomorphic contexts, characters are represented as 32-bit immediate values. In other words, a field of a constructor or structure of type `Char` does not require indirection to access. In polymorphic contexts, characters are boxed.
Expand All @@ -137,25 +137,25 @@ In monomorphic contexts, characters are represented as 32-bit immediate values.

:::comment
## API Reference
:::

## API リファレンス(API Reference)
%%%
tag := "char-api"
%%%


:::

## API リファレンス(API Reference)

:::comment
### Character Classes
:::

### 文字クラス(Character Classes)
%%%
tag := "char-api-classes"
%%%


:::

### 文字クラス(Character Classes)

{docstring Char.isAlpha}

Expand Down
Loading