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

Commit 5dcd2f6

Browse files
committed
用語対応
1 parent 0464838 commit 5dcd2f6

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

Manual/Language.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -274,7 +274,7 @@ The following data are tracked in section scopes:
274274
: The Current Namespace
275275

276276
The {deftech}_current namespace_ is the namespace into which new declarations will be defined.
277-
Additionally, {tech (key:="resolve")}[name resolution] includes all prefixes of the current namespace in the scope for global names.
277+
Additionally, {tech (key:="解決")}[name resolution]resolve includes all prefixes of the current namespace in the scope for global names.
278278

279279
: Opened Namespaces
280280

0 commit comments

Comments
 (0)