Merge pull request #121 from C-BJ/main

Translate all Japanese documents into English, simplified Chinese and traditional Chinese

CODE_OF_CONDUCT.md

@@ -1,9 +1,19 @@
 # Code of Conduct
 
-See [CODE_OF_CONDUCT](./CODE_OF_CONDUCT) Folder.
+English | <a href='./doc/CODE_OF_CONDUCT/CODE_OF_CONDUCT_JA.md'>日本語</a> | <a href='./doc/CODE_OF_CONDUCT/CODE_OF_CONDUCT_zh-CN.md'>简体中文</a> | <a href='./doc/CODE_OF_CONDUCT/CODE_OF_CONDUCT_zh-TW.md'>繁體中文</a>
 
-[CODE_OF_CONDUCT](./CODE_OF_CONDUCT)フォルダを参照してください。
+## General
 
-参见[CODE_OF_CONDUCT](./CODE_OF_CONDUCT)文件夹
+Respect others.
 
-參見[CODE_OF_CONDUCT](./CODE_OF_CONDUCT)資料夾
+Do not say mean things or show contempt, even if there is a difference in skill.
+
+Do not be aggressive in disagreements.
+
+Do not deny any identity of the other person.
+
+Do not post anything that is severely offensive to others.
+
+Do not spam, fish or troll.
+
+If you see someone who you think is violating this Code of Conduct, please contact the [administrator](mailto:moderation.erglang@gmail.com) immediately. We will take appropriate action.

CODE_OF_CONDUCT/CODE_OF_CONDUCT_EN.md

@@ -1,27 +0,0 @@
-# Code of Conduct
-
-## General
-
-Respect others.
-
-Do not say mean things or show contempt, even if there is a difference in skill.
-
-Do not be aggressive in disagreements.
-
-Do not deny any identity of the other person.
-
-Do not post anything that is severely offensive to others.
-
-Do not spam, fish or troll.
-
-If you see someone who you think is violating this Code of Conduct, please contact the [administrator](mailto:moderation.erglang@gmail.com) immediately. We will take appropriate action.
-
-## Development
-
-Requests are always welcome, but please keep in mind that they will not always be accepted. Many issues have trade-offs.
-
-Don't intercept issues that others have been assigned (Check assignees on GitHub). If it is considered too difficult for one person to handle it, we will call for more support.
-
-Before proposing a new feature, consider whether that feature could be easily solved by combining existing features.
-
-Please write code in a style that is standardized by the Erg team and languages.

CODE_OF_CONDUCT/LICENSE

@@ -1,395 +0,0 @@
-Attribution 4.0 International
-
-=======================================================================
-
-Creative Commons Corporation ("Creative Commons") is not a law firm and
-does not provide legal services or legal advice. Distribution of
-Creative Commons public licenses does not create a lawyer-client or
-other relationship. Creative Commons makes its licenses and related
-information available on an "as-is" basis. Creative Commons gives no
-warranties regarding its licenses, any material licensed under their
-terms and conditions, or any related information. Creative Commons
-disclaims all liability for damages resulting from their use to the
-fullest extent possible.
-
-Using Creative Commons Public Licenses
-
-Creative Commons public licenses provide a standard set of terms and
-conditions that creators and other rights holders may use to share
-original works of authorship and other material subject to copyright
-and certain other rights specified in the public license below. The
-following considerations are for informational purposes only, are not
-exhaustive, and do not form part of our licenses.
-
-     Considerations for licensors: Our public licenses are
-     intended for use by those authorized to give the public
-     permission to use material in ways otherwise restricted by
-     copyright and certain other rights. Our licenses are
-     irrevocable. Licensors should read and understand the terms
-     and conditions of the license they choose before applying it.
-     Licensors should also secure all rights necessary before
-     applying our licenses so that the public can reuse the
-     material as expected. Licensors should clearly mark any
-     material not subject to the license. This includes other CC-
-     licensed material, or material used under an exception or
-     limitation to copyright. More considerations for licensors:
-	wiki.creativecommons.org/Considerations_for_licensors
-
-     Considerations for the public: By using one of our public
-     licenses, a licensor grants the public permission to use the
-     licensed material under specified terms and conditions. If
-     the licensor's permission is not necessary for any reason--for
-     example, because of any applicable exception or limitation to
-     copyright--then that use is not regulated by the license. Our
-     licenses grant only permissions under copyright and certain
-     other rights that a licensor has authority to grant. Use of
-     the licensed material may still be restricted for other
-     reasons, including because others have copyright or other
-     rights in the material. A licensor may make special requests,
-     such as asking that all changes be marked or described.
-     Although not required by our licenses, you are encouraged to
-     respect those requests where reasonable. More_considerations
-     for the public:
-	wiki.creativecommons.org/Considerations_for_licensees
-
-=======================================================================
-
-Creative Commons Attribution 4.0 International Public License
-
-By exercising the Licensed Rights (defined below), You accept and agree
-to be bound by the terms and conditions of this Creative Commons
-Attribution 4.0 International Public License ("Public License"). To the
-extent this Public License may be interpreted as a contract, You are
-granted the Licensed Rights in consideration of Your acceptance of
-these terms and conditions, and the Licensor grants You such rights in
-consideration of benefits the Licensor receives from making the
-Licensed Material available under these terms and conditions.
-
-
-Section 1 -- Definitions.
-
-  a. Adapted Material means material subject to Copyright and Similar
-     Rights that is derived from or based upon the Licensed Material
-     and in which the Licensed Material is translated, altered,
-     arranged, transformed, or otherwise modified in a manner requiring
-     permission under the Copyright and Similar Rights held by the
-     Licensor. For purposes of this Public License, where the Licensed
-     Material is a musical work, performance, or sound recording,
-     Adapted Material is always produced where the Licensed Material is
-     synched in timed relation with a moving image.
-
-  b. Adapter's License means the license You apply to Your Copyright
-     and Similar Rights in Your contributions to Adapted Material in
-     accordance with the terms and conditions of this Public License.
-
-  c. Copyright and Similar Rights means copyright and/or similar rights
-     closely related to copyright including, without limitation,
-     performance, broadcast, sound recording, and Sui Generis Database
-     Rights, without regard to how the rights are labeled or
-     categorized. For purposes of this Public License, the rights
-     specified in Section 2(b)(1)-(2) are not Copyright and Similar
-     Rights.
-
-  d. Effective Technological Measures means those measures that, in the
-     absence of proper authority, may not be circumvented under laws
-     fulfilling obligations under Article 11 of the WIPO Copyright
-     Treaty adopted on December 20, 1996, and/or similar international
-     agreements.
-
-  e. Exceptions and Limitations means fair use, fair dealing, and/or
-     any other exception or limitation to Copyright and Similar Rights
-     that applies to Your use of the Licensed Material.
-
-  f. Licensed Material means the artistic or literary work, database,
-     or other material to which the Licensor applied this Public
-     License.
-
-  g. Licensed Rights means the rights granted to You subject to the
-     terms and conditions of this Public License, which are limited to
-     all Copyright and Similar Rights that apply to Your use of the
-     Licensed Material and that the Licensor has authority to license.
-
-  h. Licensor means the individual(s) or entity(ies) granting rights
-     under this Public License.
-
-  i. Share means to provide material to the public by any means or
-     process that requires permission under the Licensed Rights, such
-     as reproduction, public display, public performance, distribution,
-     dissemination, communication, or importation, and to make material
-     available to the public including in ways that members of the
-     public may access the material from a place and at a time
-     individually chosen by them.
-
-  j. Sui Generis Database Rights means rights other than copyright
-     resulting from Directive 96/9/EC of the European Parliament and of
-     the Council of 11 March 1996 on the legal protection of databases,
-     as amended and/or succeeded, as well as other essentially
-     equivalent rights anywhere in the world.
-
-  k. You means the individual or entity exercising the Licensed Rights
-     under this Public License. Your has a corresponding meaning.
-
-
-Section 2 -- Scope.
-
-  a. License grant.
-
-       1. Subject to the terms and conditions of this Public License,
-          the Licensor hereby grants You a worldwide, royalty-free,
-          non-sublicensable, non-exclusive, irrevocable license to
-          exercise the Licensed Rights in the Licensed Material to:
-
-            a. reproduce and Share the Licensed Material, in whole or
-               in part; and
-
-            b. produce, reproduce, and Share Adapted Material.
-
-       2. Exceptions and Limitations. For the avoidance of doubt, where
-          Exceptions and Limitations apply to Your use, this Public
-          License does not apply, and You do not need to comply with
-          its terms and conditions.
-
-       3. Term. The term of this Public License is specified in Section
-          6(a).
-
-       4. Media and formats; technical modifications allowed. The
-          Licensor authorizes You to exercise the Licensed Rights in
-          all media and formats whether now known or hereafter created,
-          and to make technical modifications necessary to do so. The
-          Licensor waives and/or agrees not to assert any right or
-          authority to forbid You from making technical modifications
-          necessary to exercise the Licensed Rights, including
-          technical modifications necessary to circumvent Effective
-          Technological Measures. For purposes of this Public License,
-          simply making modifications authorized by this Section 2(a)
-          (4) never produces Adapted Material.
-
-       5. Downstream recipients.
-
-            a. Offer from the Licensor -- Licensed Material. Every
-               recipient of the Licensed Material automatically
-               receives an offer from the Licensor to exercise the
-               Licensed Rights under the terms and conditions of this
-               Public License.
-
-            b. No downstream restrictions. You may not offer or impose
-               any additional or different terms or conditions on, or
-               apply any Effective Technological Measures to, the
-               Licensed Material if doing so restricts exercise of the
-               Licensed Rights by any recipient of the Licensed
-               Material.
-
-       6. No endorsement. Nothing in this Public License constitutes or
-          may be construed as permission to assert or imply that You
-          are, or that Your use of the Licensed Material is, connected
-          with, or sponsored, endorsed, or granted official status by,
-          the Licensor or others designated to receive attribution as
-          provided in Section 3(a)(1)(A)(i).
-
-  b. Other rights.
-
-       1. Moral rights, such as the right of integrity, are not
-          licensed under this Public License, nor are publicity,
-          privacy, and/or other similar personality rights; however, to
-          the extent possible, the Licensor waives and/or agrees not to
-          assert any such rights held by the Licensor to the limited
-          extent necessary to allow You to exercise the Licensed
-          Rights, but not otherwise.
-
-       2. Patent and trademark rights are not licensed under this
-          Public License.
-
-       3. To the extent possible, the Licensor waives any right to
-          collect royalties from You for the exercise of the Licensed
-          Rights, whether directly or through a collecting society
-          under any voluntary or waivable statutory or compulsory
-          licensing scheme. In all other cases the Licensor expressly
-          reserves any right to collect such royalties.
-
-
-Section 3 -- License Conditions.
-
-Your exercise of the Licensed Rights is expressly made subject to the
-following conditions.
-
-  a. Attribution.
-
-       1. If You Share the Licensed Material (including in modified
-          form), You must:
-
-            a. retain the following if it is supplied by the Licensor
-               with the Licensed Material:
-
-                 i. identification of the creator(s) of the Licensed
-                    Material and any others designated to receive
-                    attribution, in any reasonable manner requested by
-                    the Licensor (including by pseudonym if
-                    designated);
-
-                ii. a copyright notice;
-
-               iii. a notice that refers to this Public License;
-
-                iv. a notice that refers to the disclaimer of
-                    warranties;
-
-                 v. a URI or hyperlink to the Licensed Material to the
-                    extent reasonably practicable;
-
-            b. indicate if You modified the Licensed Material and
-               retain an indication of any previous modifications; and
-
-            c. indicate the Licensed Material is licensed under this
-               Public License, and include the text of, or the URI or
-               hyperlink to, this Public License.
-
-       2. You may satisfy the conditions in Section 3(a)(1) in any
-          reasonable manner based on the medium, means, and context in
-          which You Share the Licensed Material. For example, it may be
-          reasonable to satisfy the conditions by providing a URI or
-          hyperlink to a resource that includes the required
-          information.
-
-       3. If requested by the Licensor, You must remove any of the
-          information required by Section 3(a)(1)(A) to the extent
-          reasonably practicable.
-
-       4. If You Share Adapted Material You produce, the Adapter's
-          License You apply must not prevent recipients of the Adapted
-          Material from complying with this Public License.
-
-
-Section 4 -- Sui Generis Database Rights.
-
-Where the Licensed Rights include Sui Generis Database Rights that
-apply to Your use of the Licensed Material:
-
-  a. for the avoidance of doubt, Section 2(a)(1) grants You the right
-     to extract, reuse, reproduce, and Share all or a substantial
-     portion of the contents of the database;
-
-  b. if You include all or a substantial portion of the database
-     contents in a database in which You have Sui Generis Database
-     Rights, then the database in which You have Sui Generis Database
-     Rights (but not its individual contents) is Adapted Material; and
-
-  c. You must comply with the conditions in Section 3(a) if You Share
-     all or a substantial portion of the contents of the database.
-
-For the avoidance of doubt, this Section 4 supplements and does not
-replace Your obligations under this Public License where the Licensed
-Rights include other Copyright and Similar Rights.
-
-
-Section 5 -- Disclaimer of Warranties and Limitation of Liability.
-
-  a. UNLESS OTHERWISE SEPARATELY UNDERTAKEN BY THE LICENSOR, TO THE
-     EXTENT POSSIBLE, THE LICENSOR OFFERS THE LICENSED MATERIAL AS-IS
-     AND AS-AVAILABLE, AND MAKES NO REPRESENTATIONS OR WARRANTIES OF
-     ANY KIND CONCERNING THE LICENSED MATERIAL, WHETHER EXPRESS,
-     IMPLIED, STATUTORY, OR OTHER. THIS INCLUDES, WITHOUT LIMITATION,
-     WARRANTIES OF TITLE, MERCHANTABILITY, FITNESS FOR A PARTICULAR
-     PURPOSE, NON-INFRINGEMENT, ABSENCE OF LATENT OR OTHER DEFECTS,
-     ACCURACY, OR THE PRESENCE OR ABSENCE OF ERRORS, WHETHER OR NOT
-     KNOWN OR DISCOVERABLE. WHERE DISCLAIMERS OF WARRANTIES ARE NOT
-     ALLOWED IN FULL OR IN PART, THIS DISCLAIMER MAY NOT APPLY TO YOU.
-
-  b. TO THE EXTENT POSSIBLE, IN NO EVENT WILL THE LICENSOR BE LIABLE
-     TO YOU ON ANY LEGAL THEORY (INCLUDING, WITHOUT LIMITATION,
-     NEGLIGENCE) OR OTHERWISE FOR ANY DIRECT, SPECIAL, INDIRECT,
-     INCIDENTAL, CONSEQUENTIAL, PUNITIVE, EXEMPLARY, OR OTHER LOSSES,
-     COSTS, EXPENSES, OR DAMAGES ARISING OUT OF THIS PUBLIC LICENSE OR
-     USE OF THE LICENSED MATERIAL, EVEN IF THE LICENSOR HAS BEEN
-     ADVISED OF THE POSSIBILITY OF SUCH LOSSES, COSTS, EXPENSES, OR
-     DAMAGES. WHERE A LIMITATION OF LIABILITY IS NOT ALLOWED IN FULL OR
-     IN PART, THIS LIMITATION MAY NOT APPLY TO YOU.
-
-  c. The disclaimer of warranties and limitation of liability provided
-     above shall be interpreted in a manner that, to the extent
-     possible, most closely approximates an absolute disclaimer and
-     waiver of all liability.
-
-
-Section 6 -- Term and Termination.
-
-  a. This Public License applies for the term of the Copyright and
-     Similar Rights licensed here. However, if You fail to comply with
-     this Public License, then Your rights under this Public License
-     terminate automatically.
-
-  b. Where Your right to use the Licensed Material has terminated under
-     Section 6(a), it reinstates:
-
-       1. automatically as of the date the violation is cured, provided
-          it is cured within 30 days of Your discovery of the
-          violation; or
-
-       2. upon express reinstatement by the Licensor.
-
-     For the avoidance of doubt, this Section 6(b) does not affect any
-     right the Licensor may have to seek remedies for Your violations
-     of this Public License.
-
-  c. For the avoidance of doubt, the Licensor may also offer the
-     Licensed Material under separate terms or conditions or stop
-     distributing the Licensed Material at any time; however, doing so
-     will not terminate this Public License.
-
-  d. Sections 1, 5, 6, 7, and 8 survive termination of this Public
-     License.
-
-
-Section 7 -- Other Terms and Conditions.
-
-  a. The Licensor shall not be bound by any additional or different
-     terms or conditions communicated by You unless expressly agreed.
-
-  b. Any arrangements, understandings, or agreements regarding the
-     Licensed Material not stated herein are separate from and
-     independent of the terms and conditions of this Public License.
-
-
-Section 8 -- Interpretation.
-
-  a. For the avoidance of doubt, this Public License does not, and
-     shall not be interpreted to, reduce, limit, restrict, or impose
-     conditions on any use of the Licensed Material that could lawfully
-     be made without permission under this Public License.
-
-  b. To the extent possible, if any provision of this Public License is
-     deemed unenforceable, it shall be automatically reformed to the
-     minimum extent necessary to make it enforceable. If the provision
-     cannot be reformed, it shall be severed from this Public License
-     without affecting the enforceability of the remaining terms and
-     conditions.
-
-  c. No term or condition of this Public License will be waived and no
-     failure to comply consented to unless expressly agreed to by the
-     Licensor.
-
-  d. Nothing in this Public License constitutes or may be interpreted
-     as a limitation upon, or waiver of, any privileges and immunities
-     that apply to the Licensor or You, including from the legal
-     processes of any jurisdiction or authority.
-
-
-=======================================================================
-
-Creative Commons is not a party to its public
-licenses. Notwithstanding, Creative Commons may elect to apply one of
-its public licenses to material it publishes and in those instances
-will be considered the “Licensor.” The text of the Creative Commons
-public licenses is dedicated to the public domain under the CC0 Public
-Domain Dedication. Except for the limited purpose of indicating that
-material is shared under a Creative Commons public license or as
-otherwise permitted by the Creative Commons policies published at
-creativecommons.org/policies, Creative Commons does not authorize the
-use of the trademark "Creative Commons" or any other trademark or logo
-of Creative Commons without its prior written consent including,
-without limitation, in connection with any unauthorized modifications
-to any of its public licenses or any other arrangements,
-understandings, or agreements concerning use of licensed material. For
-the avoidance of doubt, this paragraph does not form part of the
-public licenses.
-
-Creative Commons may be contacted at creativecommons.org.

CONTRIBUTING.md

@@ -1,5 +1,7 @@
 # Contributing to Erg
 
+English | <a href='./doc/CONTRIBUTING/CONTRIBUTING_JA.md'>日本語</a> | <a href='./doc/CONTRIBUTING/CONTRIBUTING_zh-CN.md'>简体中文</a> | <a href='./doc/CONTRIBUTING/CONTRIBUTING_zh-TW.md'>繁體中文</a>
+
 Beginners should read the instructions [here](https://github.com/erg-lang/erg/issues/31#issuecomment-1217505198).
 
 ## Documents
@@ -25,4 +27,14 @@ We also welcome people who find that the documentation is outdated compared to o
 
 If you have any questions, please feel free to ask them on the [Discord channel](https://discord.gg/zfAAUbgGr4).
 
+## Development
+
+Requests are always welcome, but please keep in mind that they will not always be accepted. Many issues have trade-offs.
+
+Don't intercept issues that others have been assigned (Check assignees on GitHub). If it is considered too difficult for one person to handle it, we will call for more support.
+
+Before proposing a new feature, consider whether that feature could be easily solved by combining existing features.
+
+Please write code in a style that is standardized by the Erg team and languages.
+
 ## [Code of conduct](./CODE_OF_CONDUCT.md)

README.md

@@ -230,6 +230,6 @@ If you have any questions, please feel free to ask them on the [Discord channel]
 
 ## License
 
-All files in the [CODE_OF_CONDUCT](./CODE_OF_CONDUCT), [assets](./assets) and [doc](./doc) folders are licensed with [CC-BY-4.0](./doc/LICENSE). The rest of the files in this repository are licensed with [Apache License 2.0](./LICENSE-APACHE) + [MIT License](./LICENSE-MIT).
+All files in the [assets](./assets) and [doc](./doc) folders are licensed with [CC-BY-4.0](./doc/LICENSE). The rest of the files in this repository are licensed with [Apache License 2.0](./LICENSE-APACHE) + [MIT License](./LICENSE-MIT).
 
 For credits about third party crates, see [THIRD_PARTY_CREDITS.md](./THIRD_PARTY_CREDITS.md).

README_JA.md

@@ -10,11 +10,10 @@
     <a href="https://github.com/erg-lang/erg/releases"><img alt="Build status" src="https://img.shields.io/github/v/release/erg-lang/erg.svg"></a>
     <a href="https://github.com/erg-lang/erg/actions/workflows/rust.yml"><img alt="Build status" src="https://github.com/erg-lang/erg/actions/workflows/rust.yml/badge.svg"></a>
 <br>
-    <a href='./README.md'>English</a> | 日本語 | <a href='./README_zh-CN.md'>简体中文</a> | <a href='./README_zh-TW.md'>繁體中文</a>
 </p>
 
-[![badge](https://img.shields.io/endpoint.svg?url=https%3A%2F%2Fgezf7g7pd5.execute-api.ap-northeast-1.amazonaws.com%2Fdefault%2Fsource_up_to_date%3Fowner%3Derg-lang%26repos%3Derg%26ref%3Dmain%26path%3DREADME.md%26commit_hash%3D46ffc45c6890d939b97fb5aa18338d554d3a8696)
+[![badge](https://img.shields.io/endpoint.svg?url=https%3A%2F%2Fgezf7g7pd5.execute-api.ap-northeast-1.amazonaws.com%2Fdefault%2Fsource_up_to_date%3Fowner%3Derg-lang%26repos%3Derg%26ref%3Dmain%26path%3DREADME.md%26commit_hash%3Df2118ff45d9e46ca8fa44242363223be43b046dd)
-](https://gezf7g7pd5.execute-api.ap-northeast-1.amazonaws.com/default/source_up_to_date?owner=erg-lang&repos=erg&ref=main&path=README.md&commit_hash=46ffc45c6890d939b97fb5aa18338d554d3a8696)
+](https://gezf7g7pd5.execute-api.ap-northeast-1.amazonaws.com/default/source_up_to_date?owner=erg-lang&repos=erg&ref=main&path=README.md&commit_hash=f2118ff45d9e46ca8fa44242363223be43b046dd)
 
 ## Ergはこんな人におすすめです&#58;
 
@@ -230,6 +229,6 @@ nix build
 
 ## License
 
-[CODE_OF_CONDUCT](./CODE_OF_CONDUCT)、[assets](./assets)、および[doc](./doc)内のすべてのファイルは、[CC-BY-4.0](./doc/LICENSE)でライセンスされています。残りのファイルは、[Apache License 2.0](./LICENSE-APACHE) + [MIT License](./LICENSE-MIT) でライセンスされています。
+[assets](./assets)、および[doc](./doc)内のすべてのファイルは、[CC-BY-4.0](./doc/LICENSE)でライセンスされています。残りのファイルは、[Apache License 2.0](./LICENSE-APACHE) + [MIT License](./LICENSE-MIT) でライセンスされています。
 
 サードパーティーの依存ライブラリのクレジットについては、[THIRD_PARTY_CREDITS.md](./THIRD_PARTY_CREDITS.md) (英語) をご覧ください。

README_zh-CN.md

@@ -10,11 +10,10 @@
     <a href="https://github.com/erg-lang/erg/releases"><img alt="Build status" src="https://img.shields.io/github/v/release/erg-lang/erg.svg"></a>
     <a href="https://github.com/erg-lang/erg/actions/workflows/rust.yml"><img alt="Build status" src="https://github.com/erg-lang/erg/actions/workflows/rust.yml/badge.svg"></a>
 <br>
-    <a href='./README.md'>English</a> | <a href='./README_JA.md'>日本語</a> | 简体中文 | <a href='./README_zh-TW.md'>繁體中文</a>
 </p>
 
-[![badge](https://img.shields.io/endpoint.svg?url=https%3A%2F%2Fgezf7g7pd5.execute-api.ap-northeast-1.amazonaws.com%2Fdefault%2Fsource_up_to_date%3Fowner%3Derg-lang%26repos%3Derg%26ref%3Dmain%26path%3DREADME.md%26commit_hash%3D46ffc45c6890d939b97fb5aa18338d554d3a8696)
+[![badge](https://img.shields.io/endpoint.svg?url=https%3A%2F%2Fgezf7g7pd5.execute-api.ap-northeast-1.amazonaws.com%2Fdefault%2Fsource_up_to_date%3Fowner%3Derg-lang%26repos%3Derg%26ref%3Dmain%26path%3DREADME.md%26commit_hash%3Df2118ff45d9e46ca8fa44242363223be43b046dd)
-](https://gezf7g7pd5.execute-api.ap-northeast-1.amazonaws.com/default/source_up_to_date?owner=erg-lang&repos=erg&ref=main&path=README.md&commit_hash=46ffc45c6890d939b97fb5aa18338d554d3a8696)
+](https://gezf7g7pd5.execute-api.ap-northeast-1.amazonaws.com/default/source_up_to_date?owner=erg-lang&repos=erg&ref=main&path=README.md&commit_hash=f2118ff45d9e46ca8fa44242363223be43b046dd)
 
 ## Erg可以推荐给以下人员&colon;
 
@@ -233,6 +232,6 @@ nix build
 
 ## License
 
-在此存储库[CODE_OF_CONDUCT](./CODE_OF_CONDUCT)，[assets](./assets)和[doc](./doc)文件夹内的所有文件使用[CC-BY-4.0](./doc/LICENSE)授权。其余文件使用[Apache License 2.0](./LICENSE-APACHE) + [MIT License](./LICENSE-MIT)授权
+在此存储库[assets](./assets)和[doc](./doc)文件夹内的所有文件使用[CC-BY-4.0](./doc/LICENSE)授权。其余文件使用[Apache License 2.0](./LICENSE-APACHE) + [MIT License](./LICENSE-MIT)授权
 
 关于第三方crates的制作人员，请参阅：[THIRD_PARTY_CREDITS.md](./THIRD_PARTY_CREDITS.md)（英文）

README_zh-TW.md

@@ -10,11 +10,10 @@
     <a href="https://github.com/erg-lang/erg/releases"><img alt="Build status" src="https://img.shields.io/github/v/release/erg-lang/erg.svg"></a>
     <a href="https://github.com/erg-lang/erg/actions/workflows/rust.yml"><img alt="Build status" src="https://github.com/erg-lang/erg/actions/workflows/rust.yml/badge.svg"></a>
 <br>
-    <a href='./README.md'>English</a> | <a href='./README_JA.md'>日本語</a> | <a href='./README_zh-CN.md'>简体中文</a> | 繁體中文
 </p>
 
-[![badge](https://img.shields.io/endpoint.svg?url=https%3A%2F%2Fgezf7g7pd5.execute-api.ap-northeast-1.amazonaws.com%2Fdefault%2Fsource_up_to_date%3Fowner%3Derg-lang%26repos%3Derg%26ref%3Dmain%26path%3DREADME.md%26commit_hash%3D46ffc45c6890d939b97fb5aa18338d554d3a8696)
+[![badge](https://img.shields.io/endpoint.svg?url=https%3A%2F%2Fgezf7g7pd5.execute-api.ap-northeast-1.amazonaws.com%2Fdefault%2Fsource_up_to_date%3Fowner%3Derg-lang%26repos%3Derg%26ref%3Dmain%26path%3DREADME.md%26commit_hash%3Df2118ff45d9e46ca8fa44242363223be43b046dd)
-](https://gezf7g7pd5.execute-api.ap-northeast-1.amazonaws.com/default/source_up_to_date?owner=erg-lang&repos=erg&ref=main&path=README.md&commit_hash=46ffc45c6890d939b97fb5aa18338d554d3a8696)
+](https://gezf7g7pd5.execute-api.ap-northeast-1.amazonaws.com/default/source_up_to_date?owner=erg-lang&repos=erg&ref=main&path=README.md&commit_hash=f2118ff45d9e46ca8fa44242363223be43b046dd)
 
 ## Erg可以推薦給以下人員&colon;
 
@@ -233,6 +232,6 @@ nix build
 
 ## License
 
-在此存儲庫[CODE_OF_CONDUCT](./CODE_OF_CONDUCT)，[assets](./assets)和[doc](./doc)文件夾內的所有文件使用[CC-BY-4.0](./doc/LICENSE)授權。其余文件使用[Apache License 2.0](./LICENSE-APACHE) + [MIT License](./LICENSE-MIT)授權
+在此存儲庫[assets](./assets)和[doc](./doc)文件夾內的所有文件使用[CC-BY-4.0](./doc/LICENSE)授權。其余文件使用[Apache License 2.0](./LICENSE-APACHE) + [MIT License](./LICENSE-MIT)授權
 
 關於第三方crates的製作人員，請參閱：[THIRD_PARTY_CREDITS.md](./THIRD_PARTY_CREDITS.md)（英文）

compiler/erg_compiler/context/compare.rs

@@ -334,7 +334,7 @@ impl Context {
         (Maybe, false)
     }
 
-    /// ```erg
+    /// ```python
     /// assert sup_conforms(?E(<: Eq(?E)), base: Nat, sup_trait: Eq(Nat))
     /// assert sup_conforms(?E(<: Eq(?R)), base: T, sup_trait: Eq(U))
     /// ```
@@ -360,7 +360,7 @@ impl Context {
     }
 
     /// lhs :> rhs?
-    /// ```erg
+    /// ```python
     /// assert supertype_of(Int, Nat) # i: Int = 1 as Nat
     /// assert supertype_of(Bool, Bool)
     /// ```
@@ -815,7 +815,7 @@ impl Context {
     }
 
     /// see doc/LANG/compiler/refinement_subtyping.md
-    /// ```erg
+    /// ```python
     /// assert is_super_pred({I >= 0}, {I == 0})
     /// assert is_super_pred({T >= 0}, {I == 0})
     /// assert !is_super_pred({I < 0}, {I == 0})

compiler/erg_compiler/context/inquire.rs

@@ -391,7 +391,7 @@ impl Context {
     /// Just return input if the type is already concrete (or there is still a type variable that cannot be resolved)
     /// 単相化されたトレイトを具体的な型に置換する
     /// 既に具体的な型である(か、まだ型変数があり解決できない)場合はそのまま返す
-    /// ```erg
+    /// ```python
     /// instantiate_trait(Add(Int)) => Ok(Int)
     /// instantiate_trait(Array(Add(Int), 2)) => Ok(Array(Int, 2))
     /// instantiate_trait(Array(Int, 2)) => Ok(Array(Int, 2))
@@ -502,7 +502,7 @@ impl Context {
     }
 
     /// e.g.
-    /// ```erg
+    /// ```python
     /// substitute_call(instance: ((?T, ?U) -> ?T), [Int, Str], []) => instance: (Int, Str) -> Int
     /// substitute_call(instance: ((?T, Int) -> ?T), [Int, Nat], []) => instance: (Int, Int) -> Str
     /// substitute_call(instance: ((?M(: Nat)..?N(: Nat)) -> ?M+?N), [1..2], []) => instance: (1..2) -> {3}
@@ -889,7 +889,7 @@ impl Context {
     /// C3 linearization requires prior knowledge of inter-type dependencies, and cannot be used for Erg structural subtype linearization
     ///
     /// Algorithm:
-    /// ```erg
+    /// ```python
     /// [Int, Str, Nat, Never, Obj, Str!, Module]
     /// => [], [Int, Str, Nat, Never, Obj, Str!, Module]
     /// => [[Int]], [Str, Nat, Never, Obj, Str!, Module]

compiler/erg_compiler/context/mod.rs

@@ -104,7 +104,7 @@ impl TyParamIdx {
         }
     }
 
-    /// ```erg
+    /// ```python
     /// Nested(Nth(1), 0).select(F(X, G(Y, Z))) == Y
     /// ```
     pub fn select(self, from: &Type) -> Type {
@@ -246,7 +246,7 @@ pub struct Context {
     pub(crate) decls: Dict<VarName, VarInfo>,
     // stores defined names
     // 型の一致はHashMapでは判定できないため、keyはVarNameとして1つずつ見ていく
-    /// ```erg
+    /// ```python
     /// f [x, y], z = ...
     /// ```
     /// => params: vec![(None, [T; 2]), (Some("z"), U)]

compiler/erg_compiler/context/tyvar.rs

@@ -81,7 +81,7 @@ impl Context {
     }
 
     /// see doc/LANG/compiler/inference.md#一般化 for details
-    /// ```erg
+    /// ```python
     /// generalize_t(?T) == 'T: Type
     /// generalize_t(?T(<: Nat) -> ?T) == |'T <: Nat| 'T -> 'T
     /// generalize_t(?T(<: Eq(?T(<: Eq(?T(<: ...)))) -> ?T) == |'T <: Eq('T)| 'T -> 'T
@@ -258,7 +258,7 @@ impl Context {
     }
 
     /// e.g.
-    /// ```erg
+    /// ```python
     /// deref_tyvar(?T(:> Never, <: Int)[n]): ?T => Int (if self.level <= n)
     /// deref_tyvar((Int)): (Int) => Int
     /// ```
@@ -983,7 +983,7 @@ impl Context {
     /// When comparing arguments and parameter, the left side (`sub`) is the argument (found) and the right side (`sup`) is the parameter (expected)
     ///
     /// The parameter type must be a supertype of the argument type
-    /// ```erg
+    /// ```python
     /// sub_unify({I: Int | I == 0}, ?T(<: Ord)): (/* OK */)
     /// sub_unify(Int, ?T(:> Nat)): (?T :> Int)
     /// sub_unify(Nat, ?T(:> Int)): (/* OK */)

compiler/erg_compiler/effectcheck.rs

@@ -153,7 +153,7 @@ impl SideEffectChecker {
     /// returns effects, purity violations will be appended to `self.errs`.
     ///
     /// causes side-effects:
-    /// ```erg
+    /// ```python
     /// p!() // 1 side-effect
     /// p!(q!()) // 2 side-effects
     /// x =
@@ -161,12 +161,12 @@ impl SideEffectChecker {
     ///     y + 1 // 1 side-effect
     /// ```
     /// causes no side-effects:
-    /// ```erg
+    /// ```python
     /// q! = p!
     /// y = f(p!)
     /// ```
     /// purity violation:
-    /// ```erg
+    /// ```python
     /// for iter, i -> print! i
     /// ```
     fn check_expr(&mut self, expr: &Expr) {

compiler/erg_compiler/varinfo.rs

@@ -35,7 +35,7 @@ impl Mutability {
 use Mutability::*;
 
 /// e.g.
-/// ```erg
+/// ```python
 /// K(T, [U, V]) = ...
 /// U.idx == Nested(Just(1), 0)
 /// ```

compiler/erg_parser/ast.rs

@@ -2633,7 +2633,7 @@ impl Def {
 }
 
 /// e.g.
-/// ```erg
+/// ```python
 /// T = Class ...
 /// T.
 ///     x = 1

compiler/erg_parser/desugar.rs

@@ -311,12 +311,12 @@ impl Desugarer {
         todo!()
     }
 
-    /// ```erg
+    /// ```python
     /// @deco
     /// f x = ...
     /// ```
     /// ↓
-    /// ```erg
+    /// ```python
     /// _f x = ...
     /// f = deco _f
     /// ```

doc/CODE_OF_CONDUCT/CODE_OF_CONDUCT_JA.md

@@ -1,7 +1,7 @@
 # 行動規範
 
-[![badge](https://img.shields.io/endpoint.svg?url=https%3A%2F%2Fgezf7g7pd5.execute-api.ap-northeast-1.amazonaws.com%2Fdefault%2Fsource_up_to_date%3Fowner%3Derg-lang%26repos%3Derg%26ref%3Dmain%26path%3DCODE_OF_CONDUCT.md%26commit_hash%3D3ace818c1055f22f9cbe71e00f31c0aa784d52b6)
+[![badge](https://img.shields.io/endpoint.svg?url=https%3A%2F%2Fgezf7g7pd5.execute-api.ap-northeast-1.amazonaws.com%2Fdefault%2Fsource_up_to_date%3Fowner%3Derg-lang%26repos%3Derg%26ref%3Dmain%26path%3DCODE_OF_CONDUCT.md%26commit_hash%3Df2118ff45d9e46ca8fa44242363223be43b046dd)
-](https://gezf7g7pd5.execute-api.ap-northeast-1.amazonaws.com/default/source_up_to_date?owner=erg-lang&repos=erg&ref=main&path=CODE_OF_CONDUCT.md&commit_hash=3ace818c1055f22f9cbe71e00f31c0aa784d52b6)
+](https://gezf7g7pd5.execute-api.ap-northeast-1.amazonaws.com/default/source_up_to_date?owner=erg-lang&repos=erg&ref=main&path=CODE_OF_CONDUCT.md&commit_hash=f2118ff45d9e46ca8fa44242363223be43b046dd)
 
 ## 全般
 
@@ -18,13 +18,3 @@
 スパム、釣り、荒らし行為を行わないでください。
 
 この行動規範に違反していると思われる人物を見かけた場合、すぐに[管理者](mailto:moderation.erglang@gmail.com)に連絡してください。然るべき処置を行います。
-
-## 開発・実装に関して
-
-リクエストは常に受け付けますが、常に採用されるとは限らないと心に留めておいてください。多くの問題には、トレードオフが存在します。
-
-他者がアサインされたイシューを横取りするのはやめましょう(GitHubでassigneesを確認してください)。一人では手に余ると判断された場合は、さらに応援を募ります。
-
-機能の提案をする前に、その機能が既存の機能を組み合わせて容易に解決できないか考えてください。
-
-Ergチームや言語で標準とされるスタイルのコードを書いてください。

doc/CODE_OF_CONDUCT/CODE_OF_CONDUCT_zh-CN.md

@@ -1,7 +1,7 @@
 # 行为准则
 
-[![badge](https://img.shields.io/endpoint.svg?url=https%3A%2F%2Fgezf7g7pd5.execute-api.ap-northeast-1.amazonaws.com%2Fdefault%2Fsource_up_to_date%3Fowner%3Derg-lang%26repos%3Derg%26ref%3Dmain%26path%3DCODE_OF_CONDUCT.md%26commit_hash%3D3ace818c1055f22f9cbe71e00f31c0aa784d52b6)
+[![badge](https://img.shields.io/endpoint.svg?url=https%3A%2F%2Fgezf7g7pd5.execute-api.ap-northeast-1.amazonaws.com%2Fdefault%2Fsource_up_to_date%3Fowner%3Derg-lang%26repos%3Derg%26ref%3Dmain%26path%3DCODE_OF_CONDUCT.md%26commit_hash%3Df2118ff45d9e46ca8fa44242363223be43b046dd)
-](https://gezf7g7pd5.execute-api.ap-northeast-1.amazonaws.com/default/source_up_to_date?owner=erg-lang&repos=erg&ref=main&path=CODE_OF_CONDUCT.md&commit_hash=3ace818c1055f22f9cbe71e00f31c0aa784d52b6)
+](https://gezf7g7pd5.execute-api.ap-northeast-1.amazonaws.com/default/source_up_to_date?owner=erg-lang&repos=erg&ref=main&path=CODE_OF_CONDUCT.md&commit_hash=f2118ff45d9e46ca8fa44242363223be43b046dd)
 
 ## 常规
 
@@ -18,13 +18,3 @@
 不要发布垃圾邮件，钓鱼消息或恶意挑衅的帖子
 
 如果您发现有人违反了本行为准则，请立即联系 [管理员](mailto:moderation.erglang@gmail.com)。我们将采取适当的行动
-
-## 开发
-
-请求总是受欢迎的，但请记住，它们不会总是被接受。许多问题都有取舍
-
-不要拦截其他人已分配的问题（检查 GitHub 上的受理人）。如果认为一个人处理起来太困难，我们会呼吁更多的支持
-
-在提出新功能之前，请考虑通过组合现有功能是否可以轻松解决该功能
-
-请以 Erg 团队和语言标准化的风格编写代码

doc/CODE_OF_CONDUCT/CODE_OF_CONDUCT_zh-TW.md

@@ -1,7 +1,7 @@
 # 行為守則
 
-[![badge](https://img.shields.io/endpoint.svg?url=https%3A%2F%2Fgezf7g7pd5.execute-api.ap-northeast-1.amazonaws.com%2Fdefault%2Fsource_up_to_date%3Fowner%3Derg-lang%26repos%3Derg%26ref%3Dmain%26path%3DCODE_OF_CONDUCT.md%26commit_hash%3D3ace818c1055f22f9cbe71e00f31c0aa784d52b6)
+[![badge](https://img.shields.io/endpoint.svg?url=https%3A%2F%2Fgezf7g7pd5.execute-api.ap-northeast-1.amazonaws.com%2Fdefault%2Fsource_up_to_date%3Fowner%3Derg-lang%26repos%3Derg%26ref%3Dmain%26path%3DCODE_OF_CONDUCT.md%26commit_hash%3Df2118ff45d9e46ca8fa44242363223be43b046dd)
-](https://gezf7g7pd5.execute-api.ap-northeast-1.amazonaws.com/default/source_up_to_date?owner=erg-lang&repos=erg&ref=main&path=CODE_OF_CONDUCT.md&commit_hash=3ace818c1055f22f9cbe71e00f31c0aa784d52b6)
+](https://gezf7g7pd5.execute-api.ap-northeast-1.amazonaws.com/default/source_up_to_date?owner=erg-lang&repos=erg&ref=main&path=CODE_OF_CONDUCT.md&commit_hash=f2118ff45d9e46ca8fa44242363223be43b046dd)
 
 ## 常規
 
@@ -18,13 +18,3 @@
 不要發布垃圾郵件，釣魚消息或惡意挑釁的帖子
 
 如果您發現有人違反了本行為準則，請立即聯繫 [管理員](mailto:moderation.erglang@gmail.com)。我們將採取適當的行動
-
-## 開發
-
-請求總是受歡迎的，但請記住，它們不會總是被接受。許多問題都有取捨
-
-不要攔截其他人已分配的問題（檢查 GitHub 上的受理人）。如果認為一個人處理起來太困難，我們會呼籲更多的支持
-
-在提出新功能之前，請考慮通過組合現有功能是否可以輕鬆解決該功能
-
-請以 Erg 團隊和語言標準化的風格編寫代碼

doc/CONTRIBUTING/CONTRIBUTING_JA.md

@@ -0,0 +1,41 @@
+# Erg への貢献
+
+[![badge](https://img.shields.io/endpoint.svg?url=https%3A%2F%2Fgezf7g7pd5.execute-api.ap-northeast-1.amazonaws.com%2Fdefault%2Fsource_up_to_date%3Fowner%3Derg-lang%26repos%3Derg%26ref%3Dmain%26path%3DCONTRIBUTING.md%26commit_hash%3Da86bd4cd1bef4035a1ad23676c8324ab74f7b674)
+](https://gezf7g7pd5.execute-api.ap-northeast-1.amazonaws.com/default/source_up_to_date?owner=erg-lang&repos=erg&ref=main&path=CONTRIBUTING.md&commit_hash=a86bd4cd1bef4035a1ad23676c8324ab74f7b674)
+
+初心者は[こちら](https://github.com/erg-lang/erg/issues/31#issuecomment-1217505198)の説明を読んでください。
+
+## ドキュメント
+
+Erg への貢献を考えている場合は、[doc/dev_guide](./doc/EN/dev_guide/) にあるドキュメントを読む必要があります。
+または、Erg の内部構造に興味がある場合は、[doc/compiler](/doc/JA/compiler/) が役立つ情報を提供する可能性があります (現在は日本語のみ)。
+
+## バグレポート
+
+Erg のバグだと思われる動作を見つけた場合は、[報告](https://github.com/erg-lang/erg/issues/new/choose)していただければ幸いです。同じバグがまだ問題として報告されていないことを確認してください。
+
+「cargo run --features debug」と入力すると、Erg はデバッグ モードでビルドされます。このモードでは、バグの調査に役立つ情報がダンプされる場合があります。このモードでエラーログを報告していただければ幸いです。
+
+また、バグが発生した環境が原因ではないことが明らかな場合は、バグが発生した環境を報告する必要はありません。
+
+## ドキュメントの翻訳
+
+私たちは常に、ドキュメントをさまざまな言語バージョンに翻訳してくれる人を探しています。
+
+ドキュメントが他の言語に比べて古くなっていることに気づき、内容を更新したいという方も歓迎します ([こちら](https://github.com/erg-lang/erg/issues/48#issuecomment-1218247362) を参照)。これを行う方法について）。
+
+## 質問する
+
+ご不明な点がございましたら、[Discord チャンネル](https://discord.gg/zfAAUbgGr4)までお気軽にお問い合わせください。
+
+## 開発・実装に関して
+
+リクエストは常に受け付けますが、常に採用されるとは限らないと心に留めておいてください。多くの問題には、トレードオフが存在します。
+
+他者がアサインされたイシューを横取りするのはやめましょう(GitHubでassigneesを確認してください)。一人では手に余ると判断された場合は、さらに応援を募ります。
+
+機能の提案をする前に、その機能が既存の機能を組み合わせて容易に解決できないか考えてください。
+
+Ergチームや言語で標準とされるスタイルのコードを書いてください。
+
+## [行動規範](./CODE_OF_CONDUCT.md)

doc/CONTRIBUTING/CONTRIBUTING_zh-CN.md

@@ -0,0 +1,41 @@
+# 为Erg做贡献
+
+[![badge](https://img.shields.io/endpoint.svg?url=https%3A%2F%2Fgezf7g7pd5.execute-api.ap-northeast-1.amazonaws.com%2Fdefault%2Fsource_up_to_date%3Fowner%3Derg-lang%26repos%3Derg%26ref%3Dmain%26path%3DCONTRIBUTING.md%26commit_hash%3Da86bd4cd1bef4035a1ad23676c8324ab74f7b674)
+](https://gezf7g7pd5.execute-api.ap-northeast-1.amazonaws.com/default/source_up_to_date?owner=erg-lang&repos=erg&ref=main&path=CONTRIBUTING.md&commit_hash=a86bd4cd1bef4035a1ad23676c8324ab74f7b674)
+
+初学者应阅读说明 [此处](https://github.com/erg-lang/erg/issues/31#issuecomment-1217505198)。
+
+## 文档
+
+如果您正在考虑为 Erg 做贡献，您应该阅读 [doc/dev_guide](./doc/EN/dev_guide/) 下的文档。
+或者您对 Erg 的内部结构感兴趣，[doc/compiler](/doc/JA/compiler/) 可能会提供有用的信息（目前只有日语）。
+
+## 错误报告
+
+如果您发现任何您认为是 Erg 中的错误的行为，如果您愿意 [report](https://github.com/erg-lang/erg/issues/new/choose)，我将不胜感激。请确保尚未将相同的错误报告为问题。
+
+如果你输入 `cargo run --features debug`，Erg 将在调试模式下构建。此模式可能会转储可能对调查错误有用的信息。如果您能在此模式下报告错误日志，我将不胜感激。
+
+此外，如果错误明确不是由环境引起的，则不需要报告错误发生的环境。
+
+## 文档翻译
+
+我们一直在寻找将我们的文件翻译成各种语言版本的人。
+
+我们也欢迎那些发现文档与其他语言相比已经过时并希望更新内容的人（请参阅[此处](https://github.com/erg-lang/erg/issues/48#issuecomment-1218247362)如何做到这一点）。
+
+## 提问
+
+如果您有任何问题，请随时在 [Discord 频道](https://discord.gg/zfAAUbgGr4) 上提问。
+
+## 开发
+
+请求总是受欢迎的，但请记住，它们不会总是被接受。许多问题都有取舍。
+
+不要拦截其他人已分配的问题（检查 GitHub 上的受理人）。如果认为一个人处理起来太困难，我们会呼吁更多的支持。
+
+在提出新功能之前，请考虑通过组合现有功能是否可以轻松解决该功能。
+
+请以 Erg 团队和语言标准化的风格编写代码。
+
+## [行为准则](./CODE_OF_CONDUCT.md)

doc/CONTRIBUTING/CONTRIBUTING_zh-TW.md

@@ -0,0 +1,41 @@
+# 為Erg做貢獻
+
+[![badge](https://img.shields.io/endpoint.svg?url=https%3A%2F%2Fgezf7g7pd5.execute-api.ap-northeast-1.amazonaws.com%2Fdefault%2Fsource_up_to_date%3Fowner%3Derg-lang%26repos%3Derg%26ref%3Dmain%26path%3DCONTRIBUTING.md%26commit_hash%3Da86bd4cd1bef4035a1ad23676c8324ab74f7b674)
+](https://gezf7g7pd5.execute-api.ap-northeast-1.amazonaws.com/default/source_up_to_date?owner=erg-lang&repos=erg&ref=main&path=CONTRIBUTING.md&commit_hash=a86bd4cd1bef4035a1ad23676c8324ab74f7b674)
+
+初學者應閱讀說明 [此處](https://github.com/erg-lang/erg/issues/31#issuecomment-1217505198)。
+
+## 文檔
+
+如果您正在考慮為 Erg 做貢獻，您應該閱讀 [doc/dev_guide](./doc/EN/dev_guide/) 下的文檔。
+或者您對 Erg 的內部結構感興趣，[doc/compiler](/doc/JA/compiler/) 可能會提供有用的信息（目前只有日語）。
+
+## 錯誤報告
+
+如果您發現任何您認為是 Erg 中的錯誤的行為，如果您願意 [report](https://github.com/erg-lang/erg/issues/new/choose)，我將不勝感激。請確保尚未將相同的錯誤報告為問題。
+
+如果你輸入 `cargo run --features debug`，Erg 將在調試模式下構建。此模式可能會轉儲可能對調查錯誤有用的信息。如果您能在此模式下報告錯誤日誌，我將不勝感激。
+
+此外，如果錯誤明確不是由環境引起的，則不需要報告錯誤發生的環境。
+
+## 文檔翻譯
+
+我們一直在尋找將我們的文件翻譯成各種語言版本的人。
+
+我們也歡迎那些發現文檔與其他語言相比已經過時並希望更新內容的人（請參閱[此處](https://github.com/erg-lang/erg/issues/48#issuecomment-1218247362)如何做到這一點）。
+
+## 提問
+
+如果您有任何問題，請隨時在 [Discord 頻道](https://discord.gg/zfAAUbgGr4) 上提問。
+
+## 開發
+
+請求總是受歡迎的，但請記住，它們不會總是被接受。許多問題都有取捨。
+
+不要攔截其他人已分配的問題（檢查 GitHub 上的受理人）。如果認為一個人處理起來太困難，我們會呼籲更多的支持。
+
+在提出新功能之前，請考慮通過組合現有功能是否可以輕鬆解決該功能。
+
+請以 Erg 團隊和語言標準化的風格編寫代碼。
+
+## [行為準則](./CODE_OF_CONDUCT.md)

doc/EN/API/consts.md

@@ -0,0 +1,13 @@
+# built-in constants
+
+## True
+
+## False
+
+## None
+
+## Ellipsis
+
+## Not Implemented
+
+## Inf

doc/EN/API/funcs.md

@@ -0,0 +1,121 @@
+# functions
+
+## basic functions
+
+### if|T; U|(cond: Bool, then: T, else: U) -> T or U
+
+### map|T; U|(i: Iterable T, f: T -> U) -> Map U
+
+Note that the order of arguments is reversed from Python.
+
+### log(x: Object, type: LogType = Info) -> None
+
+Log `x` in debug display. Logs are summarized and displayed after the execution is finished.
+Emoji-capable terminals are prefixed according to `type`.
+
+* type == Info: 💬
+* type == Ok: ✅
+* type == Warn: ⚠️
+* type == Hint: 💡
+
+### panic(msg: Str) -> Panic
+
+Display msg and stop.
+Emoji-capable terminals have a 🚨 prefix.
+
+### discard|T|(x: ...T) -> NoneType
+
+Throw away `x`. Used when the return value is not used. Unlike `del`, it does not make the variable `x` inaccessible.
+
+```python
+p!x=
+    # Let q! return some None or non-() value
+    # use `discard` if you don't need it
+    discard q!(x)
+    f x
+
+discard True
+assert True # OK
+```
+
+### import(path: Path) -> Module or CompilerPanic
+
+Import a module. Raises a compilation error if the module is not found.
+
+### eval(code: Str) -> Object
+
+Evaluate code as code and return.
+
+### classof(object: Object) -> Class
+
+Returns the class of `object`.
+However, since classes cannot be compared, use `object in Class` instead of `classof(object) == Class` if you want to judge instances.
+The structure type determined at compile time is obtained with `Typeof`.
+
+## Iterator, Array generation system
+
+### repeat|T|(x: T) -> RepeatIterator T
+
+```python
+rep = repeat 1 # Repeater(1)
+for! rep, i =>
+    print!i
+# 1 1 1 1 1 ...
+```
+
+### dup|T; N|(x: T, N: Nat) -> [T; N]
+
+```python
+[a, b, c] = dup new(), 3
+print! a # <Object object>
+print! a == b # False
+```
+
+### cycle|T|(it: Iterable T) -> CycleIterator T
+
+```python
+cycle([0, 1]).take 4 # [0, 1, 0, 1]
+cycle("hello").take 3 # "hellohellohello"
+```
+
+## constant expression functions
+
+### Class
+
+Create a new class. Unlike `Inherit`, passing through `Class` is independent of the base type and methods are lost.
+You won't be able to compare, but you can do things like pattern matching.
+
+```python
+C = Class {i = Int}
+NewInt = ClassInt
+Months = Class 1..12
+jan = Months.new(1)
+jan + Months.new(2) # TypeError: `+` is not implemented for 'Months'
+match jan:
+    1 -> log "January"
+    _ -> log "Other"
+```
+
+The second argument, Impl, is the trait to implement.
+
+### Inherit
+
+Inherit a class. You can use the base class methods as they are.
+
+### Traits
+
+Create a new trait. Currently, only record types can be specified.
+
+### Type of
+
+Returns the argument type. Use `classof` if you want to get the runtime class.
+If you use it for type specification, Warning will appear.
+
+```python
+x: Type of i = ...
+# TypeWarning: Typeof(i) == Int, please replace it
+```
+
+### Deprecated
+
+Use as a decorator. Warn about deprecated types and functions.

doc/EN/API/modules/external/alstruct.md

@@ -0,0 +1,57 @@
+# alstruct
+
+Modules that provide traits representing algebraic structures and patches for them.
+
+* members
+
+## BinOp
+
+```python
+BinOp Op: Kind 2 = Subsume Op(Self, Self.ReturnTypeOf Op), Additional: {
+    .ReturnTypeof = TraitType -> Type
+}
+
+Nat <: BinOp Add
+assert Nat. ReturnTypeof(Add) == Nat
+assert Nat. ReturnTypeof(Sub) == Int
+assert Nat. ReturnTypeof(Mul) == Nat
+assert Nat.ReturnTypeof(Div) == Positive Ratio
+```
+
+## SemiGroup
+
+```python
+SemiGroup Op: Kind 2 = Op(Self, Self)
+
+IntIsSemiGroupAdd = Patch Int, Impl=SemiGroupAdd
+
+Int <: SemiGroup Add
+```
+
+## Functors
+
+```python
+# * Identity law: x.map(id) == x
+# * Composition law: x.map(f).map(g) == x.map(f.then g)
+Functor = Trait {
+    .map|T, U: Type| = (Self(T), T -> U) -> Self U
+}
+```
+
+## Applicative
+
+```python
+# * Identity law: x.app(X.pure(id)) == x
+Applicative = Subsume Functor, Additional: {
+    .pure|T: Type| = T -> Self T
+    .app|T, U: Type| = (Self(T), Self(T -> U)) -> Self U
+}
+```
+
+## Monad
+
+```python
+Monad = Subsume Applicative, Additional: {
+    .bind|T, U: Type| = (Self(T), T -> Self U) -> Self U
+}
+```

doc/EN/API/modules/repl.md

@@ -0,0 +1,24 @@
+# module `repl`
+
+provides REPL(Read-Eval-Print-Loop)-related APIs.
+
+## functions
+
+* `gui_help`
+
+View information about an object in a browser. Can be used offline.
+
+## types
+
+### Guess = Object
+
+#### methods
+
+* `.guess`
+
+Infers a function given its arguments and return value.
+
+```python
+1.guess((1,), 2) # <Int.__add__ method>
+[1, 2].guess((3, 4), [1, 2, 3, 4]) # <Array(T, N).concat method>
+```

doc/EN/API/modules/status.md

@@ -0,0 +1,6 @@
+# module `status`
+
+A type is defined to represent the state. Please use it by removing the option according to the situation.
+
+* ExecResult = {"success", "warning", "failure", "fatal", "unknown"}
+* ExecStatus = {"ready", "running", "sleeping", "plague", "completed", "terminated"}

doc/EN/API/modules/unit.md

@@ -0,0 +1,73 @@
+# module `unit`
+
+The `unit` module is a module that defines units that are often used in numerical calculations as types.
+Erg numeric types include `Nat`, `Int`, `Ratio`, and so on. However, these types do not have information about "what the numbers mean", so nonsense calculations such as adding meters and yards can be performed.
+By using the `unit` module, you can avoid mistakes such as passing numbers with different units to functions.
+Mistakes like this actually occur, and serious bugs such as [Mars probe missing due to wrong unit system](http://www.sydrose.com/case100/287/) can cause it.
+You should use this module if you want your code to be more robust when doing numerical computations.
+
+```python
+{*} = import "unit"
+
+x = 6m # equivalent to `x = Meter.new(6)`
+t = 3s # equivalent to `t = Sec.new(3)`
+# m/s is a velocity unit object, of type Velocity
+print! x/t # 2m/s
+print! x + 4m # 10m
+print! x + 2s # TypeError: `+`(Meter, Sec) is not implemented
+```
+
+The objects `m`, `s`, and `m/s` are called unit objects. It has the meaning of 1m, 1s, 1m/s by itself. `m/s` can be said to be a unit object created by combining m and s.
+
+In unit, the following units are defined as types. It is called SI (International System of Units).
+
+* Length: Meter (unit constant: m)
+* Mass: KiloGram (unit constant: kg, g = 0.001kg)
+* Time: Sec (minute, hour, day, year, etc. have constants such as minute, hour, day, year generated from Sec)
+* Current: Amper (unit constant: a)
+* Temperature: Kelvin (unit constant: k, Fahren, Celsius types are also available and can be converted to each other)
+* Amount of substance: Mol (unit constant: mol)
+* Luminous intensity: Candela (unit constant: cd)
+
+In addition, the types `Unit1`, `UnitMul`, and `UnitDiv` are defined, which can be used to create new units by combining basic types.
+For example, `UnitDiv(Unit1, Sec)`, because the unit of frequency hertz (hertz) is defined as the reciprocal of the vibration period (seconds).
+If you want to treat this type as a meaningful type (such as adding a dedicated method), you should create a [patch](./../../syntax/type/07_patch.md).
+
+```python
+Hertz = Patch UnitDiv(Unit1, Sec)
+SquareMeter = Patch UnitMul(Meter, Meter)
+```
+
+Some auxiliary units are also predefined.
+
+* Frequency: Hertz(hz)
+* Force: Newton(newton)
+* Energy: Joule(j)
+* Power: Watt(w)
+* Potential: Volt(v)
+* Electrical resistance: Ohm(ohm)
+* Velocity: Velocity(m/s)
+* Area: SquareMeter(m^2)
+* Volume: CubicMeter(m^3) (liter = 10e-3 m^3)
+* Angle: Degree(deg) (rad = 180/pi deg)
+* Length: Feet, Yard, Inch, Mile, Ly, Au, Angstrom
+* Weight: Pound
+
+It also defines a prefix.
+
+* Femto = 1e-15
+* Pico = 1e-12
+* Nano = 1e-9
+* Micro = 1e-6
+* Milli = 1e-3
+* Centi = 1e-2
+* Deci = 1e-1
+* Hecto = 1e+2
+* Kilo = 1e+3
+* Mega = 1e+6
+* Giga = 1e+9
+* Tera = 1e+12
+* Peta = 1e+15
+* Exa = 1e+18
+
+*Contrary to the origin of the name, Erg basically adopts the MKS unit system. If you want the unit module of the CGS unit system, please use an external library ([cgs](https://github.com/mtshiba/cgs) etc.).

doc/EN/API/modules/unsound.md

@@ -0,0 +1,24 @@
+# module `unsound`
+
+Provides APIs perform unsound and unsafe operations that cannot be guaranteed safe in Erg's type system.
+
+## `unsafe!`
+
+Executes an `Unsafe` procedure. Just like Rust, `Unsafe` APIs cannot be called directly, but are all passed as higher-order functions to this procedure.
+
+```python
+unsound = import "unsound"
+
+i = unsound. unsafe! do!:
+     # convert `Result Int` to `Int`
+     unsound.transmute input!().try_into(Int), Int
+```
+
+## transmit
+
+Converts the object of the first argument to the type of the second argument. No type checking is done.
+This function breaks the type safety of the type system. Please perform validation before using.
+
+## auto_transmute
+
+Unlike `transmute`, it automatically converts to the expected type. Works the same as Ocaml's `Obj.magic`.

doc/EN/API/operators.md

@@ -0,0 +1,64 @@
+# operator
+
+## infix operator
+
+### `_+_`|R; O; A <: Add(R, O)|(x: A, y: R) -> O
+
+Perform addition.
+
+### `_-_`|R; O; S <: Sub(R, O)|(x: S, y: R) -> O
+
+Perform subtraction.
+
+### `*`|R; O; M <: Mul R, O|(x: M, y: R) -> O
+
+Perform multiplication.
+
+### `/`|R; O; D <: Div(R, O)|(x: D, y: R) -> O
+
+Perform division.
+
+## infix alphabet operator
+
+### `and`(x: Bool, y: Bool) -> Bool
+
+Executes the and operation.
+
+### `or`(x: Bool, y: Bool) -> Bool
+
+Executes the and operation.
+
+## prefix operator
+
+### `+_`|T <: Num|(x: T) -> T
+
+Same as id by default.
+
+### `-_`|T <: Num|(x: T) -> T.Neg
+
+For example, Nat.`-`: Nat -> Neg and the return value is different.
+
+### `!`|T <: Immut|(x: T) -> `T!`
+
+Create a mutable object from an immutable object.
+This operator itself is not procedural and can be used inside a function.
+
+### `..`|T <: Ord|(x: T) -> Range T
+
+Creates a Range object with no lower bound at the end of x.
+x..x returns only x as an iterator.
+
+### `..<`|T <: Ord|(x: T) -> Range T
+
+x..<x results in an empty Range object, yielding nothing as an iterator.
+
+## postfix operator
+
+A postfix operator is called when parsing a parsing infix operator fails.
+That is, even if `x..` returns a function, `x..y` is `(..)(x, y)` and not `(x..)(y)`.
+
+### |T <: Ord|(x: T)`..` -> Range T
+
+Creates a Range object with no upper bound starting at x.
+
+### |T <: Ord|(x: T)`<..` -> Range T

doc/EN/API/procs.md

@@ -0,0 +1,39 @@
+# procedures
+
+## print!
+
+```python
+print!(x) -> NoneType
+```
+
+   Returns x with a newline.
+
+## debug!
+
+```python
+debug!(x, type = Info) -> NoneType
+```
+
+Debug x with newline (file name, line number, variable name is displayed together). Removed in release mode.
+Emoji-capable terminals are prefixed according to type.
+
+* type == Info: 💬
+* type == Ok: ✅
+* type == Warn: ⚠️
+* type == Hint: 💡
+
+## for! i: Iterable T, block: T => NoneType
+
+Traverse the iterator with the action of block.
+
+## while! cond: Bool!, block: () => NoneType
+
+Execute block while cond is True.
+
+## Lineno!() -> Nat
+
+## Filename!() -> Str
+
+## Namespace!() -> Str
+
+## Module!() -> Module

doc/EN/API/special.md

@@ -0,0 +1,175 @@
+# Special form
+
+Special forms are operators, subroutines (and the like) that cannot be expressed in the Erg type system. It is surrounded by ``, but it cannot actually be captured.
+Also, types such as `Pattern`, `Body`, and `Conv` appear for convenience, but such types do not exist. Its meaning also depends on the context.
+
+## `=`(pat: Pattern, body: Body) -> NoneType
+
+Assign body to pat as a variable. Raise an error if the variable already exists in the same scope or if it doesn't match pat.
+It is also used in record attribute definitions and default arguments.
+
+```python
+record = {i = 1; j = 2}
+f(x: Int, y = 2) = ...
+```
+
+`=` has special behavior when the body is a type or a function.
+The variable name on the left side is embedded in the object on the right side.
+
+```python
+print! Class() # <class <lambda>>
+print! x: Int -> x + 1 # <function <lambda>>
+C = Class()
+print! c # <class C>
+f = x: Int -> x + 1
+print! f # <function f>
+gx: Int = x + 1
+print! g # <function g>
+KX: Int = Class(...)
+print! K # <kind K>
+L = X: Int -> Class(...)
+print! L # <kind L>
+```
+
+The `=` operator has a return value of "undefined".
+Multiple assignments and `=` in functions result in syntax errors.
+
+```python
+i = j = 1 # SyntaxError: multiple assignments are not allowed
+print!(x=1) # SyntaxError: cannot use `=` in function arguments
+# hint: did you mean keyword arguments (`x: 1`)?
+if True, do:
+    i = 0 # SyntaxError: A block cannot be terminated by an assignment expression
+```
+
+## `->`(pat: Pattern, body: Body) -> Func
+
+Generate anonymous functions, function types.
+
+## `=>`(pat: Pattern, body: Body) -> Proc
+
+Generate anonymous procedure, procedure type.
+
+## `:`(subject, T)
+
+Determine if subject matches T. If they don't match, throw a compile error.
+
+```python
+a: Int
+f x: Int, y: Int = x / y
+```
+
+Also used for `:` applied styles.
+
+```python
+fx:
+    y
+    z
+```
+
+Like `:` and `=`, the result of the operation is undefined.
+
+```python
+_ = x: Int # SyntaxError:
+print!(x: Int) # SyntaxError:
+```
+
+## `.`(obj, attr)
+
+Read attributes of obj.
+`x.[y, z]` will return the y and z attributes of x as an array.
+
+## `|>`(obj, c: Callable)
+
+Execute `c(obj)`. `x + y |>.foo()` is the same as `(x + y).foo()`.
+
+### (x: Option T)`?` -> T | T
+
+Postfix operator. Call `x.unwrap()` and `return` immediately in case of error.
+
+## match(obj, ...lambdas: Lambda)
+
+For obj, execute lambdas that match the pattern.
+
+```python
+match[1, 2, 3]:
+  (l: Int) -> log "this is type of Int"
+  [[a], b] -> log a, b
+  [...a] -> log a
+# (one two three)
+```
+
+## del(x: ...T) -> NoneType | T
+
+Delete the variable `x`. However, built-in objects cannot be deleted.
+
+```python
+a = 1
+del a # OK
+
+del True # SyntaxError: cannot delete a built-in object
+```
+
+## do(body: Body) -> Func
+
+Generate an anonymous function with no arguments. Syntactic sugar for `() ->`.
+
+## do!(body: Body) -> Proc
+
+Generate an anonymous procedure with no arguments. Syntactic sugar for `() =>`.
+
+## `else`(l, r) -> Choice
+
+Creates a tuple-like structure of two pairs called Choice objects.
+`l, r` are evaluated lazily. That is, the expression is evaluated only when `.get_then` or `.get_else` is called.
+
+```python
+choice = 1 else 2
+assert choice.get_then() == 1
+assert choice.get_else() == 2
+assert True.then(choice) == 1
+```
+
+## set operator
+
+### `[]`(...objs)
+
+Creates an array from arguments or a dict from optional arguments.
+
+### `{}`(...objs)
+
+Create a set from arguments.
+
+### `{}`(...fields: ((Field, Value); N))
+
+Generate a record.
+
+### `{}`(layout, ...names, ...preds)
+
+Generates sieve type, rank 2 type.
+
+### `...`
+
+Expand a nested collection. It can also be used for pattern matching.
+
+```python
+[x,...y] = [1, 2, 3]
+assert x == 1 and y == [2, 3]
+assert [x, ...y] == [1, 2, 3]
+assert [...y, x] == [2, 3, 1]
+{x; ...yz} = {x = 1; y = 2; z = 3}
+assert x == 1 and yz == {y = 2; z = 3}
+assert {x; ...yz} == {x = 1; y = 2; z = 3}
+```
+
+## virtual operator
+
+Operators that cannot be used directly by the user.
+
+### ref(x: T) -> Ref T | T
+
+Returns an immutable reference to the object.
+
+### ref!(x: T!) -> Ref! T! | T!
+
+Returns a mutable reference to a mutable object.

doc/EN/API/types.md

@@ -0,0 +1,262 @@
+# List of built-in Erg types
+
+Attributes of the type itself are not stored in the `.__dict__` and cannot be referenced from the instance
+
+## Fundamental types
+
+### Objects
+
+* `__dir__`: Returns the attributes of the object as an array (dir function)
+* `__getattribute__`: get and return an attribute
+* `__hash__`: returns the hash value of the object
+* `__repr__`: string representation of the object (not rich/default implementation exists)
+* `__sizeof__`: returns the size of the object (including the size allocated in the heap)
+
+### Show
+
+* `__str__`: returns the string representation (rich) of the object
+
+### Fmt
+
+* `__format__`: Returns a formatted string
+
+### Doc
+
+* `__doc__`: object description
+
+### Named
+
+* `__name__`: the name of the object
+
+### Pickles
+
+* `__reduce__`: Serialize objects with Pickle
+* `__reduce_ex__`: __reduce__ that allows you to specify the protocol version
+
+## Object system
+
+Trait class is equivalent to ABC (abstract base class, interface) in Python
+Instance belongs to 1, True, "aaa", etc.
+Class is Int, Bool, Str, etc.
+
+### Type
+
+* `__supers__`: Supertypes (`__mro__` is an array, but this one is a Set)
+* `__basicsize__`:
+* `__dictoffset__`: not supported by Evm
+* `__flags__`:
+* `__itemsize__`: Size of instance (0 if not Class)
+* `__weakrefoffset__`: not supported by Evm
+* `__membercheck__`: equivalent to `ismember(x, T)`
+* `__subtypecheck__`: Equivalent to `issubtype(U, T)`, with alias `__subclasshook__` (compatible with CPython)
+
+### Instances
+
+* `__class__`: Returns the class from which the instance was created (automatically attached to objects created with `.new`)
+
+### Class
+
+* `__mro__`: Type array for method resolution (includes itself, always ends with Object)
+* `__base__`: base type (`__mro__[1]` if there are multiple)
+* `__new__`: instantiate
+* `__init__`: Initialize the instance
+* `__init_subclass__`: Initialize the instance
+* `__intstancecheck__`: use like `MyClass.__instancecheck__(x)`, equivalent to `isinstance(x, MyClass)`
+* `__subclasscheck__`: equivalent to `issubclass(C, MyClass)`
+
+## operator
+
+Operators other than those specified here have no special types
+
+### Eq
+
+* `__eq__(self, rhs: Self) -> Bool`: object comparison function (==)
+* `__ne__`: object comparison function (!=), with default implementation
+
+### Ord
+
+* `__lt__(self, rhs: Self) -> Bool`: Object comparison function (<)
+* `__le__`: object comparison function (<=), with default implementation
+* `__gt__`: object comparison function (>), with default implementation
+* `__ge__`: object comparison function (>=), with default implementation
+
+### Bin Add
+
+* Implements `__add__(self, rhs: Self) -> Self`: `+`
+
+### Add R
+
+* `__add__(self, rhs: R) -> Self.AddO`
+
+### Sub R
+
+* `__sub__(self, rhs: R) -> Self.SubO`
+
+### Mul R
+
+* `__mul__(self, rhs: R) -> Self.MulO`
+
+### BinMul <: Mul Self
+
+* `__pow__`: implements `**` (with default implementation)
+
+### Div R, O
+
+* Implements `__div__(self, rhs: Self) -> Self`: `/`, may panic due to 0
+
+### BinDiv <: Div Self
+
+* `__mod__`: implement `%` (with default implementation)
+
+## numeric type
+
+### Num (= Add and Sub and Mul and Eq)
+
+As an example other than Complex, Vector, Matrix, and Tensor are Num (* in Matrix and Tensor are the same as dot and product, respectively)
+
+### Complex (= Inherit(Object, Impl := Num))
+
+* `imag: Ratio`: returns the imaginary part
+* `real: Ratio`: returns the real part
+* `conjugate self -> Complex`: returns the complex conjugate
+
+### Float (= Inherit(FloatComplex, Impl := Num))
+
+### Ratio (= Inherit(Complex, Impl := Num))
+
+* `numerator: Int`: returns the numerator
+* `denominator: Int`: Returns the denominator
+
+### Int (= Inherit Ratio)
+
+### Nat (= Inherit Int)
+
+* `times!`: run the proc self times
+
+## Other basic types
+
+### Bool
+
+* `__and__`:
+* `__or__`:
+* `not`:
+
+## Str (<: Seq)
+
+* `capitalize`
+* `chomp`: remove newline characters
+* `isalnum`:
+* `isascii`:
+* `isalpha`:
+* `isdecimal`:
+* `is sight`:
+* `is identifier`
+* `islower`
+* `is numeric`
+* `isprintable`
+* `isspace`
+* `is title`
+* `isupper`
+* `lower`
+* `swapcase`
+* `title`
+* `upper`
+
+## others
+
+### Bits
+
+* `from_bytes`: Convert from Bytes
+* `to_bytes`: Convert to Bytes (specify length and endian (byteorder))
+* `bit_length`: returns bit length
+
+### Iterable T
+
+Note that it is not the type of `Iterator` itself. `Nat` is `Iterable` but you can't `Nat.next()`, you need to `Nat.iter().next()`.
+
+* `iter`: Create an Iterator.
+
+### Iterator T
+
+Nat and Range have Iterators, so `Nat.iter().map n -> n**2`, `(3..10).iter().fold (sum, n) -> sum + n*2` etc. are possible.
+Since all and any are destroyed after use, there are no side effects. These are supposed to be implemented using `next` which has no side effects, but internally `Iterator!.next!` is used for execution efficiency.
+
+* `next`: Returns the first element and the remaining Iterator.
+* `all`
+* `any`
+* `filter`
+* `filter_map`
+* `find`
+* `find_map`
+* `flat_map`
+* `flatten`
+* `fold`
+* `for_each`
+* `map`
+* `map_while`
+* `nth`
+* `pos`
+* `take`
+* `unzip`
+* `zip`
+
+### Iterator!T = IteratorT and ...
+
+* `next!`: Get the first element.
+
+## SizedIterator T = Iterator T and ...
+
+An Iterator over a finite number of elements.
+
+* `len`:
+* `chain`:
+* `count`:
+* `is_empty`:
+* `rev`:
+* `next_back`:
+* `nth_back`:
+* `rfind`:
+* `rfold`:
+* `sum`:
+* `max`:
+* `min`:
+
+## Seq T = SizedIterable T and ...
+
+* `concat`: Combine two Seqs
+* `__getitem__`: Equivalent to accessing with `[]` (otherwise panics)
+* Unlike `get`: __getitem__, it returns Option
+* `maketrans`: Create a replacement table (static method)
+* `replace`: replace
+* `translate`: replace according to the replacement table
+* `insert`: Add to idx
+* `remove`: remove idx
+* `prepend`: prepend
+* `dequeue`: remove the head
+* `push`: added to the end
+* `pop`: take the tail
+* `dedup`: remove consecutive values
+* `uniq`: Remove duplicate elements (implemented by sort |> dedup, so order may change)
+* `swap`: Swap elements
+* `reverse`: reverse elements
+* `sort`: sort elements
+* `first`:
+* `last`:
+
+### Seq! T (= Seq T and ...)
+
+* `__setitem__!`:
+* `__delitem__!`:
+* `insert!`: Add to idx
+* `remove!`: remove idx
+* `prepend!`: prepend
+* `dequeue!`: remove the beginning
+* `push!`: added to the end
+* `pop!`: take the tail
+* `dedup!`: remove consecutive values
+* `uniq!`: Remove duplicate elements (implemented by sort! |> dedup!, so order may change)
+* `swap!`: swap elements
+* `reverse!`: reverse the element
+* `set!`
+* `sort!`: sort elements
+* `translate!`

doc/EN/API/types/classes/Array!(T).md

@@ -0,0 +1,4 @@
+# Array! T
+
+A type that represents a variable-length array. Use when the length is not known at compile time. There is a syntactic sugar called `[T]!`.
+Defined by `Array! T = ArrayWithMutLength! T, !_`.

doc/EN/API/types/classes/Array(T).md

@@ -0,0 +1,3 @@
+# Array T: Type
+
+Defined by `Array T = ArrayWithLen T, _`. There is a syntactic sugar called `[T]`.

doc/EN/API/types/classes/ArrayWithLen(T,N).md

@@ -0,0 +1,34 @@
+# ArrayWithLen T: Type, N: Nat
+
+`[T; N]` is syntactic sugar. There is also an [`Array` type](./Array.md) that omits the length.
+
+## methods
+
+* values_at(self, selectors: [Nat; N]) -> [T; N]
+
+```python
+assert ["a", "b", "c", "d", "e"].values_at([0, 1, 3]) == ["a", "b", "d"]
+```
+
+* all(self, pred: T -> Bool) -> Bool
+   Returns whether all elements satisfy pred.
+   If the element is 0, it will be `True` regardless of pred, but a Warning will be issued.
+   This specification itself has been adopted by many languages and is required for logical consistency.
+
+   ```python
+   assert[].all(_ -> False)
+   ```
+
+   ```python
+   assert all(False for _in[])
+   ```
+
+## methods of ArrayWithLen T, N | T <: Eq
+
+* freq self -> [{T: Nat}]
+   Returns the frequency of occurrence of an object.
+
+```python
+assert ["a", "b", "c", "b", "c", "b"].freq() \
+== [{"a", 1}, {"b": 3}, {"c": 2}]
+```

doc/EN/API/types/classes/ArrayWithMutLength!(T,N).md

@@ -0,0 +1,34 @@
+# ArrayWithLen T: Type, N: Nat
+
+`[T; N]` is syntactic sugar. There is also an [`Array` type](./Array.md) that omits the length.
+
+## methods
+
+* values_at(self, selectors: [Nat; N]) -> [T; N]
+
+```python
+assert ["a", "b", "c", "d", "e"].values_at([0, 1, 3]) == ["a", "b", "d"]
+```
+
+* all(self, pred: T -> Bool) -> Bool
+    Returns whether all elements satisfy pred.
+    If the element is 0, it will be `True` regardless of pred, but a Warning will be issued.
+    This specification itself has been adopted by many languages and is required for logical consistency.
+
+    ```python
+    assert[].all(_ -> False)
+    ```
+
+    ```python
+    assert all(False for _in[])
+    ```
+
+## methods of ArrayWithLen T, N | T <: Eq
+
+* freq self -> [{T: Nat}]
+    Returns the frequency of occurrence of an object.
+
+```python
+assert ["a", "b", "c", "b", "c", "b"].freq() \
+== [{"a", 1}, {"b": 3}, {"c": 2}]
+```

doc/EN/API/types/classes/Complex.md

@@ -0,0 +1,14 @@
+# Complex
+
+A type that represents a complex number. Types that represent numbers in Erg, such as Float, Int, and Nat, usually have this type at the top.
+
+## supers
+
+Num and Norm
+
+## methods
+
+* abs
+* conjugate
+* imag
+* real

doc/EN/API/types/classes/Dict!.md

@@ -0,0 +1,7 @@
+# Dict! K, V
+
+A type that represents a dictionary (hashmap). There is a syntactic sugar called `{K: V}`.
+
+## methods
+
+* invert!(self) -> Self! V, K

doc/EN/API/types/classes/Either.md

@@ -0,0 +1,12 @@
+# Either L, R = L or R
+
+A type that represents "either L or R". You can think of it as a two-limited form of the Or type.
+
+## methods
+
+* orl
+* orr
+* andl
+* andr
+* mapl
+* mapr

doc/EN/API/types/classes/Float.md

@@ -0,0 +1,21 @@
+# Float size
+
+A type that represents real numbers (numbers with decimals). Represents an IEEE 754 compliant floating-point number and is the general equivalent of float in other languages.
+The size of Float size is 8(1byte)~128(16byte). A simple Float represents `Float 64`.
+0.1 in Erg actually belongs to the Ratio type, not the Float type. There is no Float type literal, it is generated by `(Ratio object)f64` (e.g. (1/2)f64, 15f64). f64 corresponds to the real number 1.
+
+## supers
+
+Complex and Ord
+
+## methods
+
+* sgn(self) -> {-1, 0, 1}
+   returns the sign.
+
+* truncate(self) -> Int
+   Returns the integer closest to itself.
+
+* separate(self) -> [Str]
+* separate(self, date: Nat) -> [Str]
+   Separate by dight digits. 3 with no arguments.

doc/EN/API/types/classes/Function(N).md

@@ -0,0 +1,9 @@
+# Function N: Nat
+
+## methods of Function 1
+
+* then(self, g: Self) -> Self
+
+```python
+assert f(g(x)) == f.then(g) x
+```

doc/EN/API/types/classes/Inf.md

@@ -0,0 +1,7 @@
+# Inf
+
+Inf is a class whose only instance is inf.
+The main use of inf is with interval types.
+For example, integer types greater than or equal to 2 are `2..<inf`, and real numbers less than or equal to 0 are `-inf<..0.0`.
+Since inf is not a number in the usual sense, the four arithmetic operations cannot be defined as it is,
+So-called extended number classes such as ExtNat are provided in the library.

doc/EN/API/types/classes/Int.md

@@ -0,0 +1,10 @@
+# Int
+
+A class that represents an integer. Instances are 0, 1, -1, 300000, etc.
+Many languages use Int (type equivalent to) even when representing natural numbers, but Erg uses the principle of use smaller types,
+It is recommended to use Nat, NZInt, Interval type, etc.
+Int is a type that comes from Python and has only `Object` as its supertype.
+
+## supers
+
+## methods

doc/EN/API/types/classes/IntRange.md

@@ -0,0 +1,19 @@
+# IntRange L, R
+
+`L..R` class.
+
+```python
+IntRange L, R: Int == L..R
+```
+
+## methods
+
+* .`_+_`: Self(L1, R1), Self(L2, R2) -> Self(L1+L2, R1+R2)
+
+normal addition. Addition of `Int` and `Nat` is defined here under the pretense that it is defined in each class.
+
+```python
+0..10 + 1..12 == 1..22
+Int + 0..10 == _..|Int|_ + 0..10 == _..|Int|_ == Int
+Nat + Nat == 0.._ + 0.._ == 0.._ == Nat
+```

doc/EN/API/types/classes/Interval.md

@@ -0,0 +1,18 @@
+# Interval begin, end := WellOrder
+
+A type that represents a subtype of the well-ordered set type (WellOrder). The Interval type has derived types such as PreOpen(x<..y).
+
+```python
+Months = 1..12
+Alphabet = "a".."z"
+Weekdays = Monday..Friday
+Winter = November..December or January..February
+```
+
+```python
+0..1 # integer range
+0.0..1.0 # real (rational) range
+# or same for 0/1..1/1
+```
+
+Computers can't handle numbers with infinite digits, so the range of real numbers is actually the range of rational numbers.

doc/EN/API/types/classes/Kind(N).md

@@ -0,0 +1,5 @@
+# Kind N: Nat
+
+```python
+Kind N: Nat = (Type; N) -> Type
+```

doc/EN/API/types/classes/Matrix.md

@@ -0,0 +1,7 @@
+# Matrix T: Num, Shape: [M, N]
+
+A type that represents a matrix. It inherits from Tensor[M, N].
+
+## def
+
+Inherit Tensor T, [M, N]

doc/EN/API/types/classes/Module.md

@@ -0,0 +1,3 @@
+# Module
+
+## methods

doc/EN/API/types/classes/Nat.md

@@ -0,0 +1,18 @@
+# Nat
+
+A type that represents a natural number. Used for array indices and range types.
+
+## def
+
+```python
+Nat = 0.._
+```
+
+## methods
+
+* times!(self, p: () => NoneType) -> NoneType
+
+```python
+100.times! () =>
+     print! "hello!"
+```

doc/EN/API/types/classes/Neg.md

@@ -0,0 +1,8 @@
+# Neg
+
+A type that represents a negative integer. Pos and Neg and {0} == Int.
+It also has some notable properties such as no division by zero and Neg * Neg == Pos.
+
+## def
+
+Inf<..-1

doc/EN/API/types/classes/Never.md

@@ -0,0 +1,13 @@
+# Never
+
+It is a subtype of all types. It is a `Class` because it has all the methods and of course `.new`. However, it does not have an instance, and the Erg stops the moment it is about to be created.
+There is also a type called `Panic` that does not have an instance, but `Never` is used for normal termination or an intentional infinite loop, and `Panic` is used for abnormal termination.
+
+```python
+# Never <: Panic
+f(): Panic = exit 0 # OK
+g(): Never = panic() # TypeError
+```
+
+The OR type of `Never`/`Panic`, eg `T or Never` can be converted to `T`. This is because `Never` is a semantically never-occurring option (if it does, the program stops immediately).
+However, when using it in the return value type of a function, `or Never` cannot be omitted because it indicates that the program may terminate.

doc/EN/API/types/classes/NonZero.md

@@ -0,0 +1,30 @@
+# NonZeroN
+
+A class that represents a non-zero number. The safety of division by zero is guaranteed.
+
+```mermaid
+class Diagram
+     class NonZero~Int~ {
+         ...
+     }
+     class Int {
+         ...
+     }
+     class Div {
+         <<trait>>
+         /(Self, R) -> O or Panic
+     }
+     class SafeDiv {
+         <<trait>>
+         /(Self, R) -> O
+     }
+     Int <|-- NonZero~Int~: Inherit
+     Div <|-- SafeDiv: Subsume
+     SafeDiv <|..NonZero~Int~: Impl
+     Div <|.. Int: Impl
+```
+
+## methods
+
+@Impl SafeDiv R, O
+.`/`: Self.(R) -> O

doc/EN/API/types/classes/Object.md

@@ -0,0 +1,7 @@
+# Objects
+
+It is the supertype of all types.
+
+## methods
+
+* __sizeof__: Nat

doc/EN/API/types/classes/Operator.md

@@ -0,0 +1,7 @@
+# Operator [...T], O
+
+is the type of the operator.
+
+##def
+
+Inherit Func [...T], O

doc/EN/API/types/classes/Option.md

@@ -0,0 +1,21 @@
+# Option T = T or NoneType
+
+A type that represents "may fail".
+
+## methods
+
+* unwrap(self, msg = "unwrapped a None value") -> T or Panic
+
+Extract it expecting the contents to be `T` type. If it is `None`, output `msg` and panic.
+
+```python
+x = "...".parse(Int).into(Option Int)
+x.unwrap() # UnwrappingError: unwrapped a None value
+x.unwrap("failed to convert from string to number") # UnwrappingError: failed to convert from string to number
+```
+
+* unwrap_or(self, else: T) -> T
+
+* unwrap_or_exec(self, f: () -> T) -> T
+
+* unwrap_or_exec!(self, p!: () => T) -> T

doc/EN/API/types/classes/Pos.md

@@ -0,0 +1,8 @@
+# Pos
+
+Pos is a type that represents positive numbers (integers greater than or equal to 1).
+Since 0 is not included, there are merits such as eliminating the possibility of division by zero.
+
+## Def
+
+`Pos = 1.._`

doc/EN/API/types/classes/Ratio.md

@@ -0,0 +1,5 @@
+#Ratio
+
+A type that represents a rational number. It is mainly used when you want to use fractions.
+In fact, the / operator in Erg returns Ratio. 1/3 etc. is not evaluated as 0.33333... and is processed as 1/3. Also, 0.1 is equivalent to 1/10. So `0.1 + 0.2 == 0.3`. It sounds obvious, but in Python it is False.
+However, the Ratio type tends to be slightly less efficient than the Float type. Float type should be used at the point where execution speed is important and the exact numerical value is not required. However, as Rob Pike says, premature optimization is the root of all evil. Do a real performance test before discarding the Ratio type and using the Float type. Amateurs unconditionally prefer lighter molds.

doc/EN/API/types/classes/Record.md

@@ -0,0 +1,14 @@
+# Record
+
+Class to which the record belongs. For example, `{i = 1}` is an element of type `Structural {i = Int}`, and is an instance of the `{i = Int}` class.
+Note that instances of other classes are elements of the record type but not instances of the record class.
+
+```python
+assert not Structural({i = Int}) in Class
+assert {i = Int} in Class
+
+C = Class {i = Int}
+c = C. new {i = 1}
+assert c in Structural {i = Int}
+assert not c in {i = Int}
+```

doc/EN/API/types/classes/Result.md

@@ -0,0 +1,7 @@
+# Result T, E
+
+```python
+Result T, E <: Error = Either T, E
+```
+
+Like `Option`, it represents "a value that may fail", but it can have the context of failure. Usage is almost the same as `Either`.

doc/EN/API/types/classes/Str!.md

@@ -0,0 +1,3 @@
+# StrWithLen!N: Nat! = Inherit StrWithLenN
+
+A type that represents a variable-length string.

doc/EN/API/types/classes/Str.md

@@ -0,0 +1,9 @@
+# Str
+
+(Invariant length) A type that represents a string. The simple `Str` type is the `StrWithLen N` type with the number of characters removed (`Str = StrWithLen _`).
+
+## methods
+
+*isnumeric
+
+Returns whether the string is an Arabic numeral. Use `isunicodenumeric` to judge kanji numerals and other characters that represent numbers (note that this behavior is different from Python).

doc/EN/API/types/classes/Subroutine.md

@@ -0,0 +1,19 @@
+# Subroutines
+
+Base type of Func and Proc.
+
+## methods
+
+* return
+
+Interrupts a subroutine and returns the specified value. Useful for quickly escaping from a nest.
+
+```python
+f x =
+     for 0..10, i ->
+         if i == 5:
+             do
+                 f::return i
+             do
+                 log i
+```

doc/EN/API/types/classes/Tensor.md

@@ -0,0 +1,24 @@
+# Tensor Shape: [Nat; N]
+
+   A class for efficiently manipulating multidimensional arrays. It also defines operations such as multiplication on multidimensional arrays.
+   Matrix, Vector, etc. inherit from this type.
+
+```python
+Tensor.arrange(0..9) #Tensor[10]
+```
+
+* reshape(self, NewShape: [Nat; M]) -> Self NewShape
+
+```python
+(1..9).into(Tensor).reshape[3, 3]
+```
+
+* identity i: Nat -> Self shape: [Nat; N]
+* zeros(Shape: [Nat; N]) -> Self
+* ones(Shape: [Nat; N]) -> Self
+
+* diag
+
+* linspace
+*logspace
+* geomspace

doc/EN/API/types/classes/TransCell(T).md

@@ -0,0 +1,12 @@
+# TransCell! T: Type!
+
+It is a cell whose contents can be changed for each mold. Since it is a subtype of T type, it also behaves as T type.
+It's useful when it's type T at initialization, and it's always type U after a certain point.
+
+```python
+a = TransCell!.new None
+a: TransCell! !NoneType
+a.set! 1
+a: TransCell! !Int
+assert a + 1 == 2
+```

doc/EN/API/types/classes/Tuple.md

@@ -0,0 +1,27 @@
+# Tuple T: ...Type
+
+A collection that holds objects of multiple types.
+
+## methods
+
+* zip self, other
+
+     Composites two ordered collections (arrays or tuples).
+
+     ```python
+     assert ([1, 2, 3].zip [4, 5, 6])[0] == (1, 4)
+     ```
+
+* zip_by self, op, other
+
+     A method that generalizes zip. You can specify a binary operation to compose.
+     `()`, `[]`, `{}`, `{:}` can also be specified as operators, and generate tuples, arrays, sets, and dicts respectively.
+
+     ```python
+     assert ([1, 2, 3].zip([4, 5, 6]))[0] == (1, 4)
+     assert ([1, 2, 3].zip_by((), [4, 5, 6]))[0] == (1, 4)
+     assert ([1, 2, 3].zip_by([], [4, 5, 6]))[0] == [1, 4]
+     assert ([1, 2, 3].zip_by({}, [4, 5, 6]))[0] == {1, 4}
+     assert ([1, 2, 3].zip_by({:}, [4, 5, 6]))[0] == {1: 4}
+     assert ([1, 2, 3].zip_by(`_+_`, [4, 5, 6]))[0] == 5
+     ```

doc/EN/API/types/classes/Vector.md

@@ -0,0 +1,3 @@
+# Vector T: Num, N: Nat
+
+A type that represents a vector. Unlike Rust and C++ types with the same name, this type only handles numbers.

doc/EN/API/types/patches/BinOp.md

@@ -0,0 +1,7 @@
+# BinOp L, R, O
+
+The type of the binary operator.
+
+## Patches
+
+Operator [L, R], O

doc/EN/API/types/patches/UnaryOp.md

@@ -0,0 +1,7 @@
+# Unary Op T, O
+
+The type of the unary operator.
+
+##def
+
+Operator [T], O

doc/EN/API/types/traits/Add(R,O).md

@@ -0,0 +1,34 @@
+# Add R
+
+```python
+Add R = Trait {
+     .AddO = Type
+     .`_+_` = (Self, R) -> Self.AddO
+}
+```
+
+`Add` is a type that defines addition. There are two types of `+` as addition: methods and functions.
+`+` as a binary function, i.e. `_+_`, is defined as follows.
+
+```python
+`_+_`(l: Add(R, O), r: R): O = l.`_+_` r
+```
+
+The purpose of this definition is so that `+` can be treated as a function instead of a method.
+
+```python
+assert [1, 2, 3].fold(0, `_+_`) == 6
+
+call op, x, y = op(x, y)
+assert call(`_+_`, 1, 2) == 3
+```
+
+Addition is typed like this.
+
+```python
+f: |O: Type; A <: Add(Int, O)| A -> O
+f x = x + 1
+
+g: |A, O: Type; Int <: Add(A, O)| A -> O
+g x = 1 + x
+```

doc/EN/API/types/traits/Div(R,O).md

@@ -0,0 +1,9 @@
+# Div R, O
+
+Use `SafeDiv` if there are no errors due to division by zero.
+
+```python
+Div R, O = Trait {
+     .`/` = Self.(R) -> O or Panic
+}
+```

doc/EN/API/types/traits/Into.md

@@ -0,0 +1,11 @@
+# Into T
+
+A type that indicates that it can be type-converted to type T.
+Even if there is no inheritance relationship between Self and T, it is defined when the relationship is convertible to each other.
+Unlike inheritance, there is no implicit conversion. You must always call the `.into` method.
+
+## methods
+
+* into(self, T) -> T
+
+   do the conversion.

doc/EN/API/types/traits/Num.md

@@ -0,0 +1,16 @@
+# Num
+
+## definition
+
+```python
+Num R = Add(R) and Sub(R) and Mul(R) and Eq
+Num = Num Self
+```
+
+## supers
+
+Add and Sub and Mul and Eq
+
+## methods
+
+*`abs`

doc/EN/API/types/traits/SafeDiv(R,O).md

@@ -0,0 +1,8 @@
+# SafeDiv R, O
+
+```python
+SafeDiv R, O = Subsume Div, {
+     @Override
+     .`/` = Self.(R) -> O
+}
+```

doc/EN/API/types/traits/Sample.md

@@ -0,0 +1,31 @@
+# Sample
+
+A trait that has a `sample` and `sample!` method that "randomly" picks an instance. The `sample` method always returns the same instance, and the `sample!` method returns a random instance that changes from call to call.
+
+Note that this is a trait that assumes that you want an appropriate instance for testing, etc., and that it is not necessarily random. If you want random sampling, use the `random` module.
+
+All major value classes implement `Sample`. It is also implemented in tuple types, record types, Or types, and sieve types that are composed of `Sample` classes.
+
+```python
+assert Int. sample() == 42
+assert Str. sample() == "example"
+# Int is sampled in 64bit range by default
+print! Int. sample!() # 1313798
+print! {x = Int; y = Int}.sample!() # {x = -32432892, y = 78458576891}
+```
+
+Below is an implementation example of `Sample`.
+
+```python
+EmailAddress = Class {header = Str; domain = Str}, Impl=Sample and Show
+@Impl Show
+Email address.
+    show self = "{self::header}@{self::domain}"
+@Impl Sample
+Email address.
+    sample(): Self = Self.new "sample@gmail.com"
+    sample!(): Self =
+        domain = ["gmail.com", "icloud.com", "yahoo.com", "outlook.com", ...].sample!()
+        header = AsciiStr. sample!()
+        Self. new {header; domain}
+```

doc/EN/API/types/traits/Unpack.md

@@ -0,0 +1,13 @@
+# Unpack
+
+marker trait. When implemented, elements can be decomposed by pattern matching like records.
+
+```python
+C = Class {i = Int}, Impl = Unpack
+C.new i = Self::new {i;}
+{i} = C.new(1)
+D = Class C or Int
+log match D.new(1):
+     (i: Int) -> i
+     ({i}: C) -> i
+```

doc/EN/compiler/TODO_hint.md

@@ -0,0 +1,4 @@
+# Hint (not implemented)
+
+* `x is not defined` (x was deleted by `Del`) => `hint: deleted in line X`
+* patch method duplication: "hint: Specify patch (like `T.foo(1)`) or delete either `.foo` using `Del`"

doc/EN/compiler/TODO_recov_suggest.md

@@ -0,0 +1,11 @@
+# Error recovery suggestions (not implemented yet)
+
+* `1 or 2`, `1 and 2` => `{1, 2}`?
+* `U = Inherit T` => Non-class type cannot be inherited, or `U = Class T`?
+* `Int and Str` => Multiple inheritance is not allowed, or `Int or Str`?
+* `: [1, 2]` => `: {1, 2}`?
+* `: [Int, 2]` => `: [Int; 2]`?
+* `[Int; Str]` => `(Int, Str)`(Tuple) or `[Int: Str]`(Dict)?
+* `{x: Int}` => `{x = Int}`?
+* `{x = Int}!` => `{x = Int!}`?
+* `ref! immut_expr` => `ref! !immut_expr`?

doc/EN/compiler/TODO_warn.md

@@ -0,0 +1,5 @@
+# warnings (not implemented yet)
+
+* `t = {(record type)}` => `T = {(record type)}`? (only types defined as constants can be used for type specification)
+* `{I: Int | ...}!` => `{I: Int! | ...}`
+* `return x`(`x != ()`) in for/while block => `f::return` (outer block)?

doc/EN/compiler/abandoned.md

@@ -0,0 +1,10 @@
+# Abandoned/rejected language specifications
+
+## Overloading (ad-hoc polymorphism)
+
+It was abandoned because it can be replaced by parametric + subtyping polymorphism, and it is incompatible with Python's semantics. See [overload](../syntax/type/overloading.md) article for details.
+
+## Ownership system with explicit lifetime
+
+It was planned to introduce an ownership system like Rust, but it was abandoned due to its incompatibility with Python's semantics and the need to introduce complicated specifications such as lifetime annotations, and all immutable objects are RC. Managed, mutable objects now have only one ownership.
+Dyne does not have a GIL like C# and Nim, and the policy is to allow value objects and low-level operations within a safe range.

doc/EN/compiler/architecture.md

@@ -2,12 +2,12 @@
 
 ## 1. Scan an Erg script (.er) and generate a `TokenStream` (parser/lex.rs)
 
-* parser/lexer/Lexer generates `TokenStream` (this is an iterator of Token, TokenStream can be generated by lexer.collect())
+* parser/lexer/Lexer generates `TokenStream` (this is an iterator of `Token`, `TokenStream` can be generated by `Lexer::collect()`)
   * `Lexer` is constructed from `Lexer::new` or `Lexer::from_str`, where `Lexer::new` reads the code from a file or command option.
   * `Lexer` can generate tokens sequentially as an iterator; if you want to get a `TokenStream` all at once, use `Lexer::lex`.
   * `Lexer` outputs `LexError`s as errors, but `LexError` does not have enough information to display itself. If you want to display the error, use the `LexerRunner` to convert the error.
   * `LexerRunner` can also be used if you want to use `Lexer` as standalone; `Lexer` is just an iterator and does not implement the `Runnable` trait.
-    * `Runnable` is implemented by `LexerRunner`, `ParserRunner`, `Compiler`, and `VirtualMachine`.
+    * `Runnable` is implemented by `LexerRunner`, `ParserRunner`, `Compiler`, and `DummyVM`.
 
 ## 2. Convert `TokenStream` -> `AST` (parser/parse.rs)
 
@@ -22,7 +22,6 @@
 ## 3. Type checking & inference, Convert `AST` -> `HIR` (compiler/lower.rs)
 
 * `HIR` has every variable's type information. It is for "High-level Intermediate Representation".
-* `HIR` only holds the type of the variable, but that's enough. In extreme cases, this is because Erg has only conversion (or operator) applications. If we know the type of the conversion, we have already know the type of the object of the argument.
 * `ASTLowerer` can be constructed in the same way as `Parser` and `Lexer`.
 * `ASTLowerer::lower` will output a tuple of `HIR` and `CompileWarnings` if no errors occur.
 * `ASTLowerer` is owned by `Compiler`. Unlike conventional structures, `ASTLowerer` handles code contexts and is not a one-time disposable.
@@ -34,8 +33,6 @@
 
 ## 5. Generate Bytecode (`CodeObj`) from `HIR` (compiler/codegen.rs)
 
-* From the type information of the expression, name resolution of the quantified subroutines will be performed.
-
 ## (6. (Future plans) Convert Bytecode -> LLVM IR)
 
 * Bytecode is stack-based, whereas LLVM IR is register-based.

doc/EN/compiler/errors.md

@@ -24,7 +24,7 @@ Raised when an attempt is made to obtain another variable reference while a borr
 
 Raised when there is an apparent non-stop cycle.
 
-```erg
+```python
 i: Int = i
 
 f(): Int = g()
@@ -91,7 +91,7 @@ Raised when the object type does not match.
 Raised when a variable is used before it is defined.
 More precisely, it occurs when a variable defined in a scope is used before it is defined.
 
-```erg
+```python
 i = 0
 f x =
     y = i + x
@@ -102,7 +102,7 @@ f x =
 In this code, the `i` in `y = i + x` is an undefined variable.
 However, if it is a constant, it can be called in another function before it is defined.
 
-```erg
+```python
 f() = g()
 g() = f()
 ```
@@ -113,7 +113,7 @@ g() = f()
 
 This happens when syntactically sound but redundant or uncommon code is detected (e.g., unnecessary `()`).
 
-```erg
+```python
 if (True): # SyntaxWarning: unnecessary parentheses
     ...
 ```

doc/EN/compiler/hir.md

@@ -0,0 +1,148 @@
+# High-level Intermediate Representation (HIR)
+
+A HIR is a struct that the Erg compiler generates from an AST.
+This struct contains the complete type information for every expression in the source code and is desugared syntactically.
+AST has a one-to-one correspondence with the source code (as plain text), but HIR has unnecessary code information removed and omitted type information added, so HIR can be converted to source code is difficult to restore.
+Let's see an example of HIR in the code below.
+
+```python
+v = ![]
+for! 0..10, i =>
+    v.push!i
+log v.sum()
+```
+
+The AST generated from this code looks like this:
+
+```python
+AST(Module[
+    VarDef{
+        sig: VarSignature {
+            pat: VarPattern::Ident(None, VarName("v")),
+            spec_t: None,
+        },
+        op: "=",
+        body: Block[
+            Unary Op {
+                op: "!",
+                expr: Array([]),
+            },
+        ],
+    },
+    Call {
+        obj: Accessor::Local("for!"),
+        args: [
+            BinOp{
+                op: "..",
+                lhs: Literal(0),
+                rhs: Literal(10),
+            },
+            Lambda{
+                sig: LambdaSignature {
+                    params: [
+                        Param Signature {
+                            pat: ParamPattern::Name(VarName("i")),
+                        },
+                    ],
+                    spec_ret_t: None,
+                },
+                body: Block[
+                    Call {
+                        obj: Accessor::Attr{"v", "push!"},
+                        args: [
+                            Accessor::Local("i"),
+                        ],
+                    },
+                ],
+            },
+        ],
+    },
+    Call {
+        obj: Accessor::Local("log"),
+        args: [
+            Call {
+                obj: Accessor::Attr("v", "sum"),
+                args: [],
+            }
+        ],
+    }
+])
+```
+
+And the HIR generated from the AST looks like this:
+
+```python
+HIR(Module[
+    VarDef{
+        sig: VarSignature {
+            pat: VarPattern::Ident(None, Name("v")),
+            t: [0..10, _]!,
+        },
+        op: "=",
+        body: Block[
+            expr: UnaryOp{
+                op: "!",
+                expr: Array([]),
+                t: [0..10, 0]!,
+            },
+        ],
+    },
+    Call {
+        obj: Accessor::Local{
+            name: "for!",
+            t: (Range Nat, Nat => NoneType) => NoneType,
+        },
+        args: [
+            BinOp{
+                op: "..",
+                lhs: Literal(0),
+                rhs: Literal(10),
+                t: 0..10,
+            },
+            Lambda{
+                sig: LambdaSignature {
+                    params: [
+                        Param Signature {
+                            pat: ParamPattern::Name(Name("i")),
+                            t: 0..10,
+                        },
+                    ],
+                    t: 0..10 => NoneType,
+                },
+                body: Block[
+                    Call {
+                        obj: Accessor::Attr{
+                            obj: Accessor::Local("v"),
+                            field: "push!",
+                            t: Ref!(Self![T ~> T, N ~> N+1]).(Nat) => NoneType,
+                        },
+                        args: [
+                            Accessor::Local("i"),
+                        ],
+                    },
+                ],
+            },
+        ],
+    },
+    Call {
+        obj: Accessor::Local{
+            name: "log",
+            t: ...Object => NoneType,
+        },
+        args: [
+            Call {
+                obj: Accessor::Attr{
+                    obj: Accessor::Local("v"),
+                    field: "sum",
+                    t: [0..10, !_] -> Nat
+                },
+                args: [],
+                t: Nat
+            }
+        ],
+    }
+])
+```
+
+Object types are inferred as small as possible. Subroutines, on the other hand, infer the type for which the implementation exists.
+Therefore, the type of the actual argument and the type of the formal argument may not match.

doc/EN/compiler/inference.md

@@ -0,0 +1,438 @@
+# type inference algorithm
+
+> __Warning__: This section is being edited and may contain some errors.
+
+The notation used below is shown.
+
+```python
+Free type variables (type, unbound): ?T, ?U, ...
+Free-type variables (values, unbound): ?a, ?b, ...
+type environment (Γ): { x: T, ... }
+Type assignment rule (S): { ?T --> T, ... }
+Type argument evaluation environment (E): { e -> e', ... }
+```
+
+Let's take the following code as an example.
+
+```python
+v = ![]
+v.push! 1
+print! v
+```
+
+Erg's type inference largely uses the Hindley-Milner type inference algorithm (although various extensions have been made). Specifically, type inference is performed by the following procedure. Terminology will be explained later.
+
+1. Infer the type of the rvalue (search)
+2. instantiate the resulting type
+3. If it is a call, perform type substitution (substitute)
+4. Resolve traits that have already been monomorphized
+5. Evaluate/reduce (eval) if there is a type variable value
+6. Remove linked type variables (deref)
+7. Propagate changes for mutable dependent methods
+8. If there is an lvalue and it is Callable, generalize the argument type (generalize)
+9. If there is an lvalue, generalize the (return value) type (generalize)
+10. If it is an assignment, register the type information in the symbol table (`Context`) (update)
+
+The specific operations are as follows.
+
+line 1. Def{sig: v, block: ![]}
+    get block type:
+        get UnaryOp type:
+            getArray type: `['T; 0]`
+            instantiate: `[?T; 0]`
+            (substitute, eval are omitted)
+    update: `Γ: {v: [?T; 0]!}`
+    expr returns `NoneType`: OK
+
+line 2. CallMethod {obj: v, name: push!, args: [1]}
+    get obj type: `Array!(?T, 0)`
+        search: `Γ Array!(?T, 0).push!({1})`
+        get: `= Array!('T ~> 'T, 'N ~> 'N+1).push!('T) => NoneType`
+        instantiate: `Array!(?T, ?N).push!(?T) => NoneType`
+        substitute(`S: {?T --> Nat, ?N --> 0}`): `Array!(Nat ~> Nat, 0 ~> 0+1).push!(Nat) => NoneType`
+        eval: `Array!(Nat, 0 ~> 1).push!({1}) => NoneType`
+        update: `Γ: {v: [Nat; 1]!}`
+    expr returns `NoneType`: OK
+
+line 3. Call {obj: print!, args: [v]}
+    get args type: `[[Nat; 1]!]`
+    get obj type:
+        search: `Γ print!([Nat; 1]!)`
+        get: `= print!(...Object) => NoneType`
+    expr returns `NoneType`: OK
+
+## Implementation of type variables
+
+Type variables were originally expressed as follows in `Type` of [ty.rs](../../src/common/ty.rs). It's now implemented in a different way, but it's essentially the same idea, so I'll consider this implementation in a more naive way.
+`RcCell<T>` is a wrapper type for `Rc<RefCell<T>>`.
+
+```rust
+pub enum Type {
+    ...
+    Var(RcCell<Option<Type>>), // a reference to the type of other expression, see docs/compiler/inference.md
+    ...
+}
+```
+
+A type variable can be implemented by keeping the entity type in an external dictionary, and the type variable itself only has its keys. However, it is said that the implementation using `RcCell` is generally more efficient (verification required, [source](https://mobile.twitter.com/bd_gfngfn/status/1296719625086877696?s=21) ).
+
+A type variable is first initialized as `Type::Var(RcCell::new(None))`.
+This type variable is rewritten as the code is analyzed, and the type is determined.
+If the content remains None until the end, it will be a type variable that cannot be determined to a concrete type (on the spot). For example, the type of `x` with `id x = x`.
+I'll call a type variable in this state an __Unbound type variable__ (I don't know the exact terminology). On the other hand, we call a variable that has some concrete type assigned to it a __Linked type variable__.
+
+Both are of the kind free type variables (the term is apparently named after "free variables"). These are type variables that the compiler uses for inference. It has such a special name because it is different from a type variable whose type is specified by the programmer, such as `'T` in `id: 'T -> 'T`.
+
+Unbound type variables are expressed as `?T`, `?U`. In the context of type theory, α and β are often used, but this one is used to simplify input.
+Note that this is a notation adopted for general discussion purposes and is not actually implemented using string identifiers.
+
+An unbound type variable `Type::Var` is replaced with a `Type::MonoQuantVar` when entering a type environment. This is called a __quantified type variable__. This is akin to the programmer-specified type variables, such as ``T``. The content is just a string, and there is no facility to link to a concrete type like a free-type variable.
+
+The operation of replacing unbound type variables with quantified type variables is called __generalization__ (or generalization). If you leave it as an unbound type variable, the type will be fixed with a single call (for example, after calling `id True`, the return type of `id 1` will be `Bool`), so It has to be generalized.
+In this way a generalized definition containing quantified type variables is registered in the type environment.
+
+## generalizations, type schemes, reifications
+
+Let's denote the operation of generalizing an unbound type variable `?T` as `gen`. Let the resulting generalized type variable be `|T: Type| T`.
+In type theory, quantified types, such as the polycorrelation type `α->α`, are distinguished by prefixing them with `∀α.` (symbols like ∀ are called (generic) quantifiers. ).
+Such a representation (e.g. `∀α.α->α`) is called a type scheme. A type scheme in Erg is denoted as `|T: Type| T -> T`.
+Type schemes are not usually considered first-class types. Configuring the type system that way can prevent type inference from working. However, in Erg, it can be regarded as a first-class type under certain conditions. See [rank2 type](../syntax/type/advanced/rank2type.md) for details.
+
+Now, when using the obtained type scheme (e.g. `'T -> 'T (id's type scheme)`) in type inference where it is used (e.g. `id 1`, `id True`), generalize must be released. This inverse transformation is called __instantiation__. We will call the operation `inst`.
+
+```python
+gen ?T = 'T
+inst 'T = ?T (?T ∉ Γ)
+```
+
+Importantly, both operations replace all occurrences of the type variable. For example, if you instantiate `'T -> 'T`, you get `?T -> ?T`.
+A replacement dict is required for instantiation, but for generalization, just link `?T` with `'T` to replace it.
+
+After that, give the type of the argument to get the target type. This operation is called type substitution, and will be denoted by `subst`.
+In addition, the operation that obtains the return type if the expression is a call is denoted as `subst_call_ret`. The first argument is a list of argument types, the second argument is the type to assign to.
+
+The type substitution rule `{?T --> X}` means to rewrite `?T` and `X` to be of the same type. This operation is called __Unification__. `X` can also be a type variable.
+A detailed unification algorithm is described in [separate section](./unification.md). We will denote the unify operation as `unify`.
+
+```python
+unify(?T, Int) == Ok(()) # ?T == (Int)
+
+# S is the type assignment rule, T is the applicable type
+subst(S: {?T --> X}, T: ?T -> ?T) == X -> X
+# Type assignment rules are {?T --> X, ?U --> T}
+subst_call_ret([X, Y], (?T, ?U) -> ?U) == Y
+```
+
+## semi-unification
+
+A variant of unification is called semi-unification (__Semi-unification__). This is the operation that updates the type variable constraints to satisfy the subtype relation.
+In some cases, type variables may or may not be unifying, hence the term "semi" unification.
+
+Semi-unification occurs, for example, during argument assignment.
+because the type of the actual argument must be a subtype of the type of the formal argument.
+If the argument type is a type variable, we need to update the subtype relation to satisfy it.
+
+```python
+# If the formal parameter type is T
+f(x: T): T = ...
+
+a: U
+# must be U <: T, otherwise type error
+f(a)
+```
+
+## Generalization
+
+Generalization is not a simple task. When multiple scopes are involved, "level management" of type variables becomes necessary.
+In order to see the necessity of level management, we first confirm that type inference without level management causes problems.
+Infer the type of the following anonymous function.
+
+```python
+x ->
+    y = x
+    y
+```
+
+First, Erg allocates type variables as follows:
+The type of y is also unknown, but is left unassigned for now.
+
+```python
+x(: ?T) ->
+    y = x
+    y
+```
+
+The first thing to determine is the type of the rvalue x. An rvalue is a "use", so we reify it.
+But the type `?T` of x is already instantiated because it is a free variable. Yo`?T` becomes the type of the rvalue.
+
+```python
+x(: ?T) ->
+    y = x (: inst ?T)
+    y
+```
+
+Generalize when registering as the type of lvalue y. However, as we will see later, this generalization is imperfect and produces erroneous results.
+
+```python
+x(: ?T) ->
+    y(:gen?T) = x(:?T)
+    y
+```
+
+```python
+x(: ?T) ->
+    y(: 'T) = x
+    y
+```
+
+The type of y is now a quantified type variable `'T`. In the next line, `y` is used immediately. Concrete.
+
+```python
+x: ?T ->
+    y(: 'T) = x
+    y(: inst 'T)
+```
+
+Note that instantiation must create a (free) type variable that is different from any (free) type variables that already exist (generalization is similar). Such type variables are called fresh type variables.
+
+```python
+x: ?T ->
+    y = x
+    y(: ?U)
+```
+
+And look at the type of the resulting whole expression. `?T -> ?U`.
+But obviously this expression should be `?T -> ?T`, so we know there is a problem with the reasoning.
+This happened because we didn't "level manage" the type variables.
+
+So we introduce the level of type variables with the following notation. Levels are expressed as natural numbers.
+
+```python
+# normal type variable
+?T<1>, ?T<2>, ...
+# type variable with subtype constraint
+?T<1>(<:U) or ?T(<:U)<1>, ...
+```
+
+Let's try again.
+
+```python
+x ->
+    y = x
+    y
+```
+
+First, assign a leveled type variable as follows: The toplevel level is 1. As the scope gets deeper, the level increases.
+Function arguments belong to an inner scope, so they are one level higher than the function itself.
+
+```python
+# level 1
+x (: ?T<2>) ->
+    # level 2
+    y = x
+    y
+```
+
+First, instantiate the rvalue `x`. Same as before, nothing changed.
+
+```python
+x (: ?T<2>) ->
+    y = x (: inst ?T<2>)
+    y
+```
+
+Here is the key. This is a generalization when assigning to the type of lvalue `y`.
+Earlier, the results were strange here, so we will change the generalization algorithm.
+If the level of the type variable is less than or equal to the level of the current scope, generalization leaves it unchanged.
+
+```python
+gen ?T<n> = if n <= current_level, then= ?T<n>, else= 'T
+```
+
+```python
+x (: ?T<2>) ->
+    # current_level = 2
+    y(: gen ?T<2>) = x(: ?T<2>)
+    y
+```
+
+That is, the lvalue `y` has type `?T<2>`.
+
+```python
+x (: ?T<2>) ->
+    # ↓ not generalized
+    y(: ?T<2>) = x
+    y
+```
+
+The type of y is now an unbound type variable `?T<2>`. Concrete with the following lines: but the type of `y` is not generalized, so nothing happens.
+
+```python
+x (: ?T<2>) ->
+    y(: ?T<2>) = x
+    y (: inst ?T<2>)
+```
+
+```python
+x (: ?T<2>) ->
+    y = x
+    y (: ?T<2>)
+```
+
+We successfully got the correct type `?T<2> -> ?T<2>`.
+
+Let's see another example. This is the more general case, with function/operator application and forward references.
+
+```python
+fx, y = id(x) + y
+id x = x
+
+f10,1
+```
+
+Let's go through it line by line.
+
+During the inference of `f`, the later defined function constant `id` is referenced.
+In such a case, insert a hypothetical declaration of `id` before `f` and assign a free-type variable to it.
+Note that the level of the type variable at this time is `current_level`. This is to avoid generalization within other functions.
+
+```python
+id: ?T<1> -> ?U<1>
+f x (: ?V<2>), y (: ?W<2>) =
+    id(x) (: subst_call_ret([inst ?V<2>], inst ?T<1> -> ?U<1>)) + y
+```
+
+Unification between type variables replaces higher-level type variables with lower-level type variables.
+It doesn't matter which one if the level is the same.
+
+Semiunification between type variables is a little different.
+Type variables at different levels must not impose type constraints on each other.
+
+```python
+# BAD
+f x (: ?V<2>), y (: ?W<2>) =
+    # ?V<2>(<: ?T<1>)
+    # ?T<1>(:> ?V<2>)
+    id(x) (: ?U<1>) + y (: ?W<2>)
+```
+
+This makes it impossible to determine where to instantiate the type variable.
+For Type type variables, normal unification is performed instead of semi-unification.
+In other words, unify to the lower level.
+
+```python
+# OK
+f x (: ?V<2>), y (: ?W<2>) =
+    # ?V<2> --> ?T<1>
+    id(x) (: ?U<1>) + y (: ?W<2>)
+```
+
+```python
+f x (: ?T<1>), y (: ?W<2>) =
+    (id(x) + x): subst_call_ret([inst ?U<1>, inst ?W<2>], inst |'L <: Add('R)| ('L, 'R) -> 'L .AddO)
+```
+
+```python
+f x (: ?T<1>), y (: ?W<2>) =
+    (id(x) + x): subst_call_ret([inst ?U<1>, inst ?W<2>], (?L(<: Add(?R<2>))<2>, ?R<2 >) -> ?L<2>.AddO)
+```
+
+```python
+id: ?T<1> -> ?U<1>
+f x (: ?T<1>), y (: ?W<2>) =
+    # ?U<1>(<: Add(?W<2>)) # Inherit the constraints of ?L
+    # ?L<2> --> ?U<1>
+    # ?R<2> --> ?W<2> (not ?R(:> ?W), ?W(<: ?R))
+    (id(x) + x) (: ?U<1>.AddO)
+```
+
+```python
+# current_level = 1
+f(x, y) (: gen ?T<1>, gen ?W<2> -> gen ?U<1>.AddO) =
+    id(x) + x
+```
+
+```python
+id: ?T<1> -> ?U<1>
+f(x, y) (: |'W: Type| (?T<1>, 'W) -> gen ?U<1>(<: Add(?W<2>)).AddO) =
+    id(x) + x
+```
+
+```python
+f(x, y) (: |'W: Type| (?T<1>, 'W) -> ?U<1>(<: Add(?W<2>)).AddO) =
+    id(x) + x
+```
+
+When defining, raise the level so that it can be generalized.
+
+```python
+# ?T<1 -> 2>
+# ?U<1 -> 2>
+id x (: ?T<2>) -> ?U<2> = x (: inst ?T<2>)
+```
+
+If the return type has already been assigned, unify with the resulting type (`?U<2> --> ?T<2>`).
+
+```python
+# ?U<2> --> ?T<2>
+f(x, y) (: |'W: Type| (?T<2>, 'W) -> ?T<2>(<: Add(?W<2>)).AddO) =
+    id(x) + x
+# current_level = 1
+id(x) (: gen ?T<2> -> gen ?T<2>) = x (: ?T<2>)
+```
+
+If the type variable has been instantiated into a simple Type variable,
+The type variable that depends on it will also be a Type type variable.
+Generalized type variables are independent for each function.
+
+```python
+f(x, y) (: |'W: Type, 'T <: Add('W)| ('T, 'W) -> 'T.AddO) =
+    id(x) + x
+id(x) (: |'T: Type| 'T -> gen 'T) = x
+```
+
+```python
+f x, y (: |'W: Type, 'T <: Add('W)| ('T, 'W) -> 'T.AddO) =
+    id(x) + y
+id(x) (: 'T -> 'T) = x
+
+f(10, 1) (: subst_call_ret([inst {10}, inst {1}], inst |'W: Type, 'T <: Add('W)| ('T, 'W) -> 'T .AddO)
+```
+
+```python
+f(10, 1) (: subst_call_ret([inst {10}, inst {1}], (?T<1>(<: Add(?W<1>)), ?W<1>) -> ? T<1>.AddO))
+```
+
+Type variables are bounded to the smallest type that has an implementation.
+
+```python
+# ?T(:> {10} <: Add(?W<1>))<1>
+# ?W(:> {1})<1>
+# ?W(:> {1})<1> <: ?T<1> (:> {10}, <: Add(?W(:> {1})<1>))
+# serialize
+# {1} <: ?W<1> or {10} <: ?T<1> <: Add({1}) <: Add(?W<1>)
+# The minimal implementation trait for Add(?W)(:> ?V) is Add(Nat) == Nat, since Add is covariant with respect to the first argument
+# {10} <: ?W<1> or {1} <: ?T<1> <: Add(?W<1>) <: Add(Nat) == Nat
+# ?T(:> ?W(:> {10}) or {1}, <: Nat).AddO == Nat # If there is only one candidate, finalize the evaluation
+f(10, 1) (: (?W(:> {10}, <: Nat), ?W(:> {1})) -> Nat)
+# This is the end of the program, so remove the type variable
+f(10, 1) (: ({10}, {1}) -> Nat)
+```
+
+The resulting type for the entire program is:
+
+```python
+f|W: Type, T <: Add(W)|(x: T, y: W): T.AddO = id(x) + y
+id|T: Type|(x: T): T = x
+
+f(10, 1): Nat
+```
+
+I've also reprinted the original, unexplicitly typed program.
+
+```python
+fx, y = id(x) + y
+id x = x
+
+f(10, 1)
+```

doc/EN/compiler/overview.md

@@ -1,36 +1,36 @@
-# Overview of `erg
+# overview of `erg`
 
-This section introduces the function of each layer and especially important functions and methods.
+We will introduce the function of each layer and the particularly important functions and methods.
 
-## 1. Lexical analysis
+## 1. Lexical Analysis
 
-* `Lexer` performs lexical analysis. `Lexer::next` (`Lexer` is implemented as an iterator) handles the main logic of lexical analysis. `Token` is output as a result of parsing.
+* The `Lexer` does the lexical analysis. `Lexer::next` (`Lexer` is implemented as an iterator) is responsible for the main logic of lexical analysis. `Token` is output as a result of parsing.
 
 ## 2. Parsing
 
-* `Parser` performs the parsing. Especially important is `Parser::parse_expr`. The result of parsing is `AST`, a collection of `ast::Expr`.
+* `Parser` does the parsing. Of particular importance is `Parser::parse_expr`. As a result of parsing, `AST` which is a collection of `ast::Expr` is output.
 
 ## 3. Desugaring
 
-* `Desugarer` performs desugaring. An `AST` is output.
+* Desugaring is done by `Desugarer`. `AST` will be output.
 
 ## 4. Type checking/type inference
 
-* `ASTLowerer` performs typing. Type checking is mainly done by `Context`. Of particular importance are `Context::supertype_of` (to determine subtype relationships), `Context::unify/sub_unify` (to unify/semi-unify type variables) and `Context::init_builtin_*` (to define built-in API). The `HIR` is output as a result of the analysis.
+* `ASTLowerer` does the typing. Type checking is primarily done by the `Context`. Especially important are `Context::supertype_of` (determine subtype relation), `Context::unify/sub_unify` (unify/semi-unify type variables), `Context::init_builtin_*`( defines built-in APIs). `HIR` is output as a result of analysis.
 
-## 5. Side Effect Check
+## 5. Side effect check
 
-* `SideEffectChecker` does this.
+* `SideEffectChecker` does.
 
 ## 6. Ownership check
 
-* Performed by `OwnershipChecker`.
+* `OwnershipChecker` does.
 
-## 7. Bytecode generation
+## 7. Bytecode Generation
 
-* `CodeGenerator` converts `HIR` to `CodeObj`. The `CodeObj` holds the bytecode and execution settings. Especially important is `CodeGenerator::compile_expr`.
+* `CodeGenerator` converts `HIR` to `CodeObj`. `CodeObj` holds bytecode and execution configuration. Of particular importance is `CodeGenerator::compile_expr`.
 
 ---
 
-* All the above processes are put together by `Compiler` as a facade.
+* All the above processing is put together by the `Compiler` as a facade.
-* Execution of the generated bytecode is of course done by Python, which is called by `DummyVM`.
+* Of course Python executes the generated bytecode, which is called `DummyVM`.

doc/EN/compiler/parsing.md

@@ -5,7 +5,7 @@
 A peculiarity of Erg's grammar is that it is space-sensitive.
 This is to compensate for the loss of expressiveness caused by the omission of `()`. A similar syntax is found in Nim, which also allows the omission of `()`.
 
-```erg
+```python
 f +1 == f(+1)
 f + 1 == `+`(f, 1)
 f (1,) == f((1,))
@@ -20,7 +20,7 @@ In Erg, left-hand side values are not as simple as the left-hand side of `=`.
 In fact, there is (very confusingly) a right-sided value on the left side of `=`, and a left-sided value on the right side of `=`.
 There can even be a left-side value within a right-side value.
 
-```erg
+```python
 # i is the left-hand side value, Array(Int) and [1, 2, 3] are the right-hand side values
 i: Array(Int) = [1, 2, 3]
 # `[1, 2, 3].iter().map i -> i + 1` is the right-hand side value, but i to the left of -> is the left-hand side value

doc/EN/compiler/refinement_subtyping.md

@@ -0,0 +1,149 @@
+# Sieve type
+
+The sieve type is the following type.
+
+```python
+{I: Int | I >= 0}
+{S: StrWithLen N | N >= 1}
+{T: (Ratio, Ratio) | T.0 >= 0; T.1 >= 0}
+```
+
+Erg enables type determination by converting Enum and Interval types into sieve types.
+
+## Convert to sieve type
+
+In the section [Sieve types], we said that interval types and enum types are syntactic sugar for sieve types. Each is converted as follows.
+
+* {0} -> {I: Int | I == 0}
+* {0, 1} -> {I: Int | I == 0 or I == 1}
+* 1.._ -> {I: Int | I >= 1}
+* 1<.._ -> {I: Int | I > 1} -> {I: Int | I >= 2}
+* {0} or 1.._ -> {I: Int | I == 0 or I >= 1}
+* {0} or {-3, -2} or 1.._ -> {I: Int | I == 0 or (I == -2 or I == -3) or I >= 1}
+* {0} and {-3, 0} -> {I: Int | I == 0 and (I == -3 or I == 0)}
+* {0} not {-3, 0} or 1.._ -> {I: Int | I == 0 and not (I == -3 or I == 0) or I >= 1}
+
+## Sieve type detection
+
+An algorithm for determining whether a sieve type A is a subtype of another sieve type B is described. Formally, (all) subtyping is defined as follows:
+
+```console
+A <: B <=> ∀a∈A; a ∈ B
+```
+
+Specifically, the following inference rules are applied. Boolean expressions are assumed to be simplified.
+
+* intervalization rules (done automatically from type definition)
+  * `Nat` => `{I: Int | I >= 0}`
+* Round-up rule
+  * `{I: Int | I < n}` => `{I: Int | I <= n-1}`
+  * `{I: Int | I > n}` => `{I: Int | I >= n+1}`
+  * `{R: Ratio | R < n}` => `{R: Ratio | R <= n-ε}`
+  * `{R: Ratio | R > n}` => `{R: Ratio | R >= n+ε}`
+* reversal rule
+  * `{A not B}` => `{A and (not B)}`
+* De Morgan's Law
+  * `{not (A or B)}` => `{not A and not B}`
+  * `{not (A and B)}` => `{not A or not B}`
+* Distribution rule
+  * `{A and (B or C)} <: D` => `{(A and B) or (A and C)} <: D` => `({A and B} <: D) and ( {A and C} <: D)`
+  * `{(A or B) and C} <: D` => `{(C and A) or (C and B)} <: D` => `({C and A} <: D) and ( {C and B} <: D)`
+  * `D <: {A or (B and C)}` => `D <: {(A or B) and (A or C)}` => `(D <: {A or B}) and ( D <: {A or C})`
+  * `D <: {(A and B) or C}` => `D <: {(C or A) and (C or B)}` => `(D <: {C or A}) and ( D <: {C or B})`
+  * `{A or B} <: C` => `({A} <: C) and ({B} <: C)`
+  * `A <: {B and C}` => `(A <: {B}) and (A <: {C})`
+* termination rule
+  * {I: T | ...} <: T = True
+  * {} <: _ = True
+  * _ <: {...} = True
+  * {...} <: _ = False
+  * _ <: {} == False
+  * {I >= a and I <= b} (a < b) <: {I >= c} = (a >= c)
+  * {I >= a and I <= b} (a < b) <: {I <= d} = (b <= d)
+  * {I >= a} <: {I >= c or I <= d} (c >= d) = (a >= c)
+  * {I <= b} <: {I >= c or I <= d} (c >= d) = (b <= d)
+  * {I >= a and I <= b} (a <= b) <: {I >= c or I <= d} (c > d) = ((a >= c) or (b <= d ))
+  * basic formula
+    * {I >= l} <: {I >= r} = (l >= r)
+    * {I <= l} <: {I <= r} = (l <= r)
+    * {I >= l} <: {I <= r} = False
+    * {I <= l} <: {I >= r} = False
+
+The simplification rules for Boolean expressions are as follows. min, max may not be removed. Also, multiple or, and are converted to nested min, max.
+
+* ordering rules
+  * `I == a` => `I >= a and I <= a`
+  * `i != a` => `I >= a+1 or I <= a-1`
+* Consistency rule
+  * `I >= a or I <= b (a < b)` == `{...}`
+* Constancy rule
+  * `I >= a and I <= b (a > b)` == `{}`
+* replacement rule
+  * Replace order expressions in the order `I >= n` and `I <= n`.
+* Extension rule
+  * `I == n or I >= n+1` => `I >= n`
+  * `I == n or I <= n-1` => `I <= n`
+* maximum rule
+  * `I <= m or I <= n` => `I <= max(m, n)`
+  * `I >= m and I >= n` => `I >= max(m, n)`
+* minimum rule
+  * `I >= m or I >= n` => `I >= min(m, n)`
+  * `I <= m and I <= n` => `I <= min(m, n)`
+* elimination rule
+  * `I == n` on the left side is removed when `I >= a (n >= a)` or `I <= b (n <= b)` or `I == n` on the right side can.
+  * False if all left-hand equations cannot be eliminated
+
+e.g.
+
+```python
+1.._<: Nat
+=> {I: Int | I >= 1} <: {I: Int | I >= 0}
+=> {I >= 1} <: {I >= 0}
+=> (I >= 0 => I >= 1)
+=> 1 >= 0
+=> True
+# {I >= l} <: {I >= r} == (l >= r)
+# {I <= l} <: {I <= r} == (l <= r)
+```
+
+```python
+{I: Int | I >= 0} <: {I: Int | I >= 1 or I <= -3}
+=> {I >= 0} <: {I >= 1 or I <= -3}
+=> {I >= 0} <: {I >= 1} or {I >= 0} <: {I <= -3}
+=> False or False
+=> False
+```
+
+```python
+{I: Int | I >= 0} <: {I: Int | I >= -3 and I <= 1}
+=> {I >= 0} <: {I >= -3 and I <= 1}
+=> {I >= 0} <: {I >= -3} and {I >= 0} <: {I <= 1}
+=> True and False
+=> False
+```
+
+```python
+{I: Int | I >= 2 or I == -2 or I <= -4} <: {I: Int | I >= 1 or I <= -1}
+=> {I >= 2 or I <= -4 or I == -2} <: {I >= 1 or I <= -1}
+=> {I >= 2 or I <= -4} <: {I >= 1 or I <= -1}
+    and {I == -2} <: {I >= 1 or I <= -1}
+=> {I >= 2} <: {I >= 1 or I <= -1}
+        and {I <= -4} <: {I >= 1 or I <= -1}
+    and
+        {I == -2} <: {I >= 1}
+        or {I == -2} <: {I <= -1}
+=> {I >= 2} <: {I >= 1}
+        or {I >= 2} <: {I <= -1}
+    and
+        {I <= -4} <: {I >= 1}
+        or {I <= -4} <: {I <= -1}
+    and
+        False or True
+=> True or False
+    and
+        False or True
+    and
+        True
+=> True and True
+=> True
+```

doc/EN/compiler/trait_method_resolving.md

@@ -0,0 +1,95 @@
+# Resolving patch methods
+
+`Nat` is zero or more `Int`, a subtype of `Int`.
+`Nat` does not exist in the Python class hierarchy. I wonder how Erg solves this patch method?
+
+```python
+1.times do:
+    log "hello world"
+```
+
+`.times` is a `NatImpl` patch method.
+Since `1` is an instance of `Int`, it is first searched by tracing the MRO (Method Resolution Order) of `Int`.
+Erg has `Int`, `Object` in the MRO of `Int`. It comes from Python (`int.__mro__ == [int, object]` in Python).
+The `.times` method does not exist in either of them. Now let's explore that subtype.
+
+~
+
+Integers should obviously have reals, complexes, and even whole numbers in their supertypes, but that fact does not appear in the Python-compatible layer.
+However, `1 in Complex` and `1 in Num` are actually `True` in Erg.
+As for `Complex`, even though it is a class that does not have an inheritance relationship with `Int`, it is judged to be compatible as a type. What the hell is going on?
+
+~
+
+An object has an infinite number of types to which it belongs.
+But we really only have to think about types with methods, i.e. types with names.
+
+The Erg compiler has a hashmap of patch types with all provided methods and their implementations.
+This table is updated each time a new type is defined.
+
+```python
+provided_method_table = {
+    ...
+    "foo": [Foo],
+    ...
+    ".times": [Nat, Foo],
+    ...
+}
+```
+
+Types that have a `.times` method are `Nat`, `Foo`. From among these, find one that matches the `{1}` type.
+There are two types of conformity determination. They are sieve-type judgment and record-type judgment. This is done from the sieve type determination.
+
+## Sieve type determination
+
+Check if the candidate type is compatible with the type `{1}` of `1`. The sieve types compatible with `{1}` are `{0, 1}`, `0..9`, and so on.
+Finite element algebraic types such as `0..1 or 3..4`, `-1..2 and 0..3` are normalized to sieve types when declared as base types (i.e. ` {0, 1, 3, 4}`, `{0, 1, 2}`).
+In this case, `Nat` is `0.._ == {I: Int | I >= 0}`, so `{1}` is compatible with `Nat`.
+
+## Determine record type
+
+Check if the candidate type is compatible with `Int`, a class of 1.
+Others that are patches of `Int` and that `Int` has all the required attributes are also compatible.
+
+~
+
+So `Nat` fit. However, if `Foo` also matches, it is determined by the containment relationship between `Nat` and `Foo`.
+That is, subtype methods are selected.
+If there is no containment relationship between the two, a compile error will occur (this is a safety measure against executing a method against the programmer's intention).
+To eliminate the error, you need to specify the patch explicitly.
+
+```python
+o.method(x) -> P.method(o, x)
+```
+
+## method resolution for universal patches
+
+Define a patch like this:
+
+```python
+FnType T: Type = Patch T -> T
+FnType.type = T
+```
+
+Code like the following is possible under the `FnType` patch. I wonder how this will be resolved.
+
+```python
+assert (Int -> Int).type == Int
+```
+
+First, `FnType(T)` is registered in `provided_method_table` in the following format.
+
+```python
+provided_method_table = {
+    ...
+    "type": [FnType(T)],
+    ...
+}
+```
+
+`FnType(T)` is checked for matching types. In this case, `FnType(T)` patch type is `Type -> Type`.
+This matches `Int -> Int`. If it fits, do monomorphization and replace (take a diff of `T -> T` and `Int -> Int`, `{T => Int}`).
+
+```python
+assert FnType(Int).type == Int
+```

doc/EN/compiler/transpile.md

@@ -0,0 +1,90 @@
+# How is Erg code transpiled to Python code?
+
+To be precise, Erg code is transpiled to Python bytecode.
+However, since Python bytecode can almost be reconstructed into Python code, the equivalent Python code is used as an example here.
+By the way, the example presented here is a low optimization level.
+More advanced optimizations eliminate things that don't need to be instantiated.
+
+## Record, Record type
+
+It will be transpiled to a namedtuple.
+For namedtuple, see [here](https://docs.python.jp/3/library/collections.html#collections.namedtuple).
+There is a similar function, dataclass, but dataclass has a slight performance drop due to auto-implementation of `__eq__` and `__hash__`.
+
+```python
+Employee = Class {.name = Str; .id = Int}
+
+employee = Employee.new({.name = "John Smith"; .id = 100})
+
+assert employee.name == "John Smith"
+```
+
+```python
+from typing import NamedTuple
+
+class Employee(NamedTuple):
+    __records__ = ['name', 'id']
+    name: str
+    id: int
+
+employee = Employee('John Smith', 100)
+
+assert employee.name == 'John Smith'
+```
+
+It will also be converted to a simple tuple if it can be further optimized.
+
+## Polymorphic Type
+
+> WIPs
+
+## Instant Scope
+
+If no namespace conflicts occur, it will simply be mangled and expanded.
+Names such as `x::y` are used in bytecode and cannot be associated with Python code, but if you force it to be expressed, it will be as follows.
+
+```python
+x =
+    y = 1
+    y+1
+```
+
+```python
+x::y = 1
+x = x::y + 1
+```
+
+In case of conflict, define and use a function that can only be referenced internally.
+
+```python
+x =
+    y = 1
+    y+1
+```
+
+```python
+def _():
+    x=1
+    y = x
+    return y + 1
+x = _()
+```
+
+## Visibility
+
+It does nothing for public variables as it is Python's default.
+Private variables are handled by mangling.
+
+```python
+x=1
+y =
+    x = 2
+    assert module::x == 2
+```
+
+```python
+module::x = 1
+y::x = 2
+assert module::x == 2
+y = None
+```