Improve the English translation of doc and increase the simplified Chinese translation of doc

2025-08-04 10:49:54 +00:00 · 2022-09-04 07:20:19 +08:00 · 2022-09-04 07:20:19 +08:00 · d15cbbf7b3
commit d15cbbf7b3
parent 00493160e2
319 changed files with 17672 additions and 893 deletions
--- a/doc/EN/API/consts.md
+++ b/doc/EN/API/consts.md
@ -0,0 +1,13 @@
+# built-in constants
+
+## True
+
+## False
+
+## None
+
+## Ellipsis
+
+## Not Implemented
+
+## Inf
--- a/doc/EN/API/funcs.md
+++ b/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.
+
+``` erg
+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
+
+``` erg
+rep = repeat 1 # Repeater(1)
+for! rep, i =>
+    print!i
+# 1 1 1 1 1 ...
+```
+
+### dup|T; N|(x: T, N: Nat) -> [T; N]
+
+``` erg
+[a, b, c] = dup new(), 3
+print! a # <Object object>
+print! a == b # False
+```
+
+### cycle|T|(it: Iterable T) -> CycleIterator T
+
+``` erg
+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.
+
+``` erg
+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.
+
+``` erg
+x: Type of i = ...
+# TypeWarning: Typeof(i) == Int, please replace it
+```
+
+### Deprecated
+
+Use as a decorator. Warn about deprecated types and functions.
--- a/doc/EN/API/index.md
+++ b/doc/EN/API/index.md
--- a/doc/EN/API/modules/external/alstruct.md
+++ b/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
+
+``` erg
+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
+
+``` erg
+SemiGroup Op: Kind 2 = Op(Self, Self)
+
+IntIsSemiGroupAdd = Patch Int, Impl=SemiGroupAdd
+
+Int <: SemiGroup Add
+```
+
+## Functors
+
+``` erg
+## * 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
+
+``` erg
+## * 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
+
+``` erg
+Monad = Subsume Applicative, Additional: {
+    .bind|T, U: Type| = (Self(T), T -> Self U) -> Self U
+}
+```
--- a/doc/EN/API/modules/repl.md
+++ b/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.
+
+``` erg
+1.guess((1,), 2) # <Int.__add__ method>
+[1, 2].guess((3, 4), [1, 2, 3, 4]) # <Array(T, N).concat method>
+```
--- a/doc/EN/API/modules/status.md
+++ b/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"}
--- a/doc/EN/API/modules/unit.md
+++ b/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.
+
+``` erg
+{*} = 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).
+
+``` erg
+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.).
--- a/doc/EN/API/modules/unsound.md
+++ b/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.
+
+``` erg
+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`.
--- a/doc/EN/API/operators.md
+++ b/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
--- a/doc/EN/API/procs.md
+++ b/doc/EN/API/procs.md
@ -0,0 +1,39 @@
+# procedures
+
+## print!
+
+``` erg
+print!(x) -> NoneType
+```
+
+   Returns x with a newline.
+
+##debug&excl;
+
+``` erg
+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
--- a/doc/EN/API/special.md
+++ b/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.
+
+``` erg
+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.
+
+``` erg
+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.
+
+``` erg
+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.
+
+``` erg
+a: Int
+f x: Int, y: Int = x / y
+```
+
+Also used for `:` applied styles.
+
+``` erg
+fx:
+    y
+    z
+```
+
+Like `:` and `=`, the result of the operation is undefined.
+
+``` erg
+_ = 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.
+
+``` erg
+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.
+
+``` erg
+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.
+
+``` erg
+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.
+
+``` erg
+[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.
--- a/doc/EN/API/types.md
+++ b/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!`
--- a/doc/EN/API/types/classes/Array!(T).md
+++ b/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, !_`.
--- a/doc/EN/API/types/classes/Array(T).md
+++ b/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]`.
--- a/doc/EN/API/types/classes/ArrayWithLen(T,N).md
+++ b/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]
+
+``` erg
+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.
+
+   ``` erg
+   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.
+
+``` erg
+assert ["a", "b", "c", "b", "c", "b"].freq() \
+== [{"a", 1}, {"b": 3}, {"c": 2}]
+```
--- a/doc/EN/API/types/classes/ArrayWithMutLength!(T,N).md
+++ b/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]
+
+``` erg
+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.
+
+    ``` erg
+    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.
+
+``` erg
+assert ["a", "b", "c", "b", "c", "b"].freq() \
+== [{"a", 1}, {"b": 3}, {"c": 2}]
+```
--- a/doc/EN/API/types/classes/Class.md
+++ b/doc/EN/API/types/classes/Class.md
--- a/doc/EN/API/types/classes/Complex.md
+++ b/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
--- a/doc/EN/API/types/classes/Dict!.md
+++ b/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
--- a/doc/EN/API/types/classes/Either.md
+++ b/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
--- a/doc/EN/API/types/classes/Float.md
+++ b/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.
--- a/doc/EN/API/types/classes/Function(N).md
+++ b/doc/EN/API/types/classes/Function(N).md
@ -0,0 +1,9 @@
+# Function N: Nat
+
+## methods of Function 1
+
+* then(self, g: Self) -> Self
+
+``` erg
+assert f(g(x)) == f.then(g) x
+```
--- a/doc/EN/API/types/classes/Inf.md
+++ b/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.
--- a/doc/EN/API/types/classes/Int.md
+++ b/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
--- a/doc/EN/API/types/classes/IntRange.md
+++ b/doc/EN/API/types/classes/IntRange.md
@ -0,0 +1,19 @@
+# IntRange L, R
+
+`L..R` class.
+
+``` erg
+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.
+
+``` erg
+0..10 + 1..12 == 1..22
+Int + 0..10 == _..|Int|_ + 0..10 == _..|Int|_ == Int
+Nat + Nat == 0.._ + 0.._ == 0.._ == Nat
+```
--- a/doc/EN/API/types/classes/Interval.md
+++ b/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).
+
+``` erg
+Months = 1..12
+Alphabet = "a".."z"
+Weekdays = Monday..Friday
+Winter = November..December or January..February
+```
+
+``` erg
+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.
--- a/doc/EN/API/types/classes/Iterator.md
+++ b/doc/EN/API/types/classes/Iterator.md
--- a/doc/EN/API/types/classes/Kind(N).md
+++ b/doc/EN/API/types/classes/Kind(N).md
@ -0,0 +1,5 @@
+# Kind N: Nat
+
+```erg
+Kind N: Nat = (Type; N) -> Type
+```
--- a/doc/EN/API/types/classes/Matrix.md
+++ b/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]
--- a/doc/EN/API/types/classes/Module.md
+++ b/doc/EN/API/types/classes/Module.md
@ -0,0 +1,3 @@
+# Module
+
+## methods
--- a/doc/EN/API/types/classes/Nat.md
+++ b/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
+
+``` erg
+Nat = 0.._
+```
+
+## methods
+
+* times!(self, p: () => NoneType) -> NoneType
+
+``` erg
+100.times! () =>
+     print! "hello!"
+```
--- a/doc/EN/API/types/classes/Neg.md
+++ b/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
--- a/doc/EN/API/types/classes/Never.md
+++ b/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.
+
+``` erg
+# 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.
--- a/doc/EN/API/types/classes/NonZero.md
+++ b/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
--- a/doc/EN/API/types/classes/Object.md
+++ b/doc/EN/API/types/classes/Object.md
@ -0,0 +1,7 @@
+# Objects
+
+It is the supertype of all types.
+
+## methods
+
+* __sizeof__: Nat
--- a/doc/EN/API/types/classes/Operator.md
+++ b/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
--- a/doc/EN/API/types/classes/Option.md
+++ b/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.
+
+``` erg
+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
--- a/doc/EN/API/types/classes/Pos.md
+++ b/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.._`
--- a/doc/EN/API/types/classes/Ratio.md
+++ b/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.
--- a/doc/EN/API/types/classes/Record.md
+++ b/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.
+
+``` erg
+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}
+```
--- a/doc/EN/API/types/classes/Result.md
+++ b/doc/EN/API/types/classes/Result.md
@ -0,0 +1,7 @@
+# Result T, E
+
+``` erg
+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`.
--- a/doc/EN/API/types/classes/Str!.md
+++ b/doc/EN/API/types/classes/Str!.md
@ -0,0 +1,3 @@
+# StrWithLen!N: Nat! = Inherit StrWithLenN
+
+A type that represents a variable-length string.
--- a/doc/EN/API/types/classes/Str.md
+++ b/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).
--- a/doc/EN/API/types/classes/StrWithLen.md
+++ b/doc/EN/API/types/classes/StrWithLen.md
--- a/doc/EN/API/types/classes/Subroutine.md
+++ b/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.
+
+``` erg
+f x =
+     for 0..10, i ->
+         if i == 5:
+             do
+                 f::return i
+             do
+                 log i
+```
--- a/doc/EN/API/types/classes/Tensor.md
+++ b/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.
+
+``` erg
+Tensor.arrange(0..9) #Tensor[10]
+```
+
+* reshape(self, NewShape: [Nat; M]) -> Self NewShape
+
+``` erg
+(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
--- a/doc/EN/API/types/classes/TransCell(T).md
+++ b/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.
+
+``` erg
+a = TransCell!.new None
+a: TransCell! !NoneType
+a.set! 1
+a: TransCell! !Int
+assert a + 1 == 2
+```
--- a/doc/EN/API/types/classes/Tuple.md
+++ b/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).
+
+     ``` erg
+     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.
+
+     ``` erg
+     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
+     ```
--- a/doc/EN/API/types/classes/Type.md
+++ b/doc/EN/API/types/classes/Type.md
--- a/doc/EN/API/types/classes/Vector.md
+++ b/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.
--- a/doc/EN/API/types/patches/BinOp.md
+++ b/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
--- a/doc/EN/API/types/patches/UnaryOp.md
+++ b/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
--- a/doc/EN/API/types/traits/Add(R,O).md
+++ b/doc/EN/API/types/traits/Add(R,O).md
@ -0,0 +1,34 @@
+# Add R
+
+``` erg
+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.
+
+``` erg
+`_+_`(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.
+
+``` erg
+assert [1, 2, 3].fold(0, `_+_`) == 6
+
+call op, x, y = op(x, y)
+assert call(`_+_`, 1, 2) == 3
+```
+
+Addition is typed like this.
+
+``` erg
+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
+```
--- a/doc/EN/API/types/traits/Div(R,O).md
+++ b/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.
+
+``` erg
+Div R, O = Trait {
+     .`/` = Self.(R) -> O or Panic
+}
+```
--- a/doc/EN/API/types/traits/Eq.md
+++ b/doc/EN/API/types/traits/Eq.md
--- a/doc/EN/API/types/traits/Into.md
+++ b/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.
--- a/doc/EN/API/types/traits/Iterable.md
+++ b/doc/EN/API/types/traits/Iterable.md
--- a/doc/EN/API/types/traits/Num.md
+++ b/doc/EN/API/types/traits/Num.md
@ -0,0 +1,16 @@
+# Num
+
+## definition
+
+``` erg
+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`
--- a/doc/EN/API/types/traits/Ord.md
+++ b/doc/EN/API/types/traits/Ord.md
--- a/doc/EN/API/types/traits/SafeDiv(R,O).md
+++ b/doc/EN/API/types/traits/SafeDiv(R,O).md
@ -0,0 +1,8 @@
+# SafeDiv R, O
+
+``` erg
+SafeDiv R, O = Subsume Div, {
+     @Override
+     .`/` = Self.(R) -> O
+}
+```
--- a/doc/EN/API/types/traits/Sample.md
+++ b/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.
+
+``` erg
+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`.
+
+``` erg
+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}
+```
--- a/doc/EN/API/types/traits/Seq.md
+++ b/doc/EN/API/types/traits/Seq.md
--- a/doc/EN/API/types/traits/Show.md
+++ b/doc/EN/API/types/traits/Show.md
--- a/doc/EN/API/types/traits/Unpack.md
+++ b/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.
+
+``` erg
+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
+```
--- a/doc/EN/compiler/TODO_hint.md
+++ b/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`"
--- a/doc/EN/compiler/TODO_recov_suggest.md
+++ b/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`?
--- a/doc/EN/compiler/TODO_warn.md
+++ b/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)?
--- a/doc/EN/compiler/abandoned.md
+++ b/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.
--- a/doc/EN/compiler/hir.md
+++ b/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.
+
+``` erg
+v = ![]
+for! 0..10, i =>
+    v.push!i
+log v.sum()
+```
+
+The AST generated from this code looks like this:
+
+``` erg
+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:
+
+``` erg
+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.
--- a/doc/EN/compiler/index.md
+++ b/doc/EN/compiler/index.md
--- a/doc/EN/compiler/inference.md
+++ b/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.
+
+``` erg
+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.
+
+``` erg
+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`.
+
+``` erg
+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`.
+
+``` erg
+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.
+
+``` erg
+# 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.
+
+``` erg
+x ->
+    y = x
+    y
+```
+
+First, Erg allocates type variables as follows:
+The type of y is also unknown, but is left unassigned for now.
+
+``` erg
+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.
+
+``` erg
+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.
+
+``` erg
+x(: ?T) ->
+    y(:gen?T) = x(:?T)
+    y
+```
+
+``` erg
+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.
+
+``` erg
+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.
+
+``` erg
+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.
+
+``` erg
+# normal type variable
+?T<1>, ?T<2>, ...
+# type variable with subtype constraint
+?T<1>(<:U) or ?T(<:U)<1>, ...
+```
+
+Let's try again.
+
+``` erg
+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.
+
+``` erg
+# level 1
+x (: ?T<2>) ->
+    # level 2
+    y = x
+    y
+```
+
+First, instantiate the rvalue `x`. Same as before, nothing changed.
+
+``` erg
+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.
+
+``` erg
+gen ?T<n> = if n <= current_level, then= ?T<n>, else= 'T
+```
+
+``` erg
+x (: ?T<2>) ->
+    # current_level = 2
+    y(: gen ?T<2>) = x(: ?T<2>)
+    y
+```
+
+That is, the lvalue `y` has type `?T<2>`.
+
+``` erg
+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.
+
+``` erg
+x (: ?T<2>) ->
+    y(: ?T<2>) = x
+    y (: inst ?T<2>)
+```
+
+``` erg
+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.
+
+``` erg
+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.
+
+``` erg
+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.
+
+``` erg
+# 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.
+
+``` erg
+# OK
+f x (: ?V<2>), y (: ?W<2>) =
+    # ?V<2> --> ?T<1>
+    id(x) (: ?U<1>) + y (: ?W<2>)
+```
+
+``` erg
+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)
+```
+
+``` erg
+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)
+```
+
+``` erg
+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)
+```
+
+``` erg
+# current_level = 1
+f(x, y) (: gen ?T<1>, gen ?W<2> -> gen ?U<1>.AddO) =
+    id(x) + x
+```
+
+``` erg
+id: ?T<1> -> ?U<1>
+f(x, y) (: |'W: Type| (?T<1>, 'W) -> gen ?U<1>(<: Add(?W<2>)).AddO) =
+    id(x) + x
+```
+
+``` erg
+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.
+
+``` erg
+# ?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>`).
+
+``` erg
+# ?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.
+
+``` erg
+f(x, y) (: |'W: Type, 'T <: Add('W)| ('T, 'W) -> 'T.AddO) =
+    id(x) + x
+id(x) (: |'T: Type| 'T -> gen 'T) = x
+```
+
+``` erg
+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)
+```
+
+``` erg
+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.
+
+``` erg
+# ?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:
+
+``` erg
+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.
+
+``` erg
+fx, y = id(x) + y
+id x = x
+
+f(10, 1)
+```
--- a/doc/EN/compiler/overview.md
+++ b/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.
-* Execution of the generated bytecode is of course done by Python, which is called by `DummyVM`.
+* All the above processing is put together by the `Compiler` as a facade.
+* Of course Python executes the generated bytecode, which is called `DummyVM`.
--- a/doc/EN/compiler/refinement_subtyping.md
+++ b/doc/EN/compiler/refinement_subtyping.md
@ -0,0 +1,149 @@
+# Sieve type
+
+The sieve type is the following type.
+
+``` erg
+{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
+```
--- a/doc/EN/compiler/trait_method_resolving.md
+++ b/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?
+
+``` erg
+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.
+
+``` erg
+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.
+
+``` erg
+o.method(x) -> P.method(o, x)
+```
+
+## method resolution for universal patches
+
+Define a patch like this:
+
+``` erg
+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.
+
+``` erg
+assert (Int -> Int).type == Int
+```
+
+First, `FnType(T)` is registered in `provided_method_table` in the following format.
+
+``` erg
+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}`).
+
+``` erg
+assert FnType(Int).type == Int
+```
--- a/doc/EN/compiler/transpile.md
+++ b/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__`.
+
+``` erg
+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.
+
+``` erg
+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.
+
+``` erg
+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.
+
+``` erg
+x=1
+y =
+    x = 2
+    assert module::x == 2
+```
+
+```python
+module::x = 1
+y::x = 2
+assert module::x == 2
+y = None
+```
--- a/doc/EN/compiler/type_var_normalization.md
+++ b/doc/EN/compiler/type_var_normalization.md
@ -0,0 +1,39 @@
+# Normalization
+
+* Erg's type argument normalization is based on SymPy's simplify function.
+
+For example, when you define `concat: |T, M, N|([T; M], [T; N] -> [T; M+N])`, you can match type variables and arguments without instantiating them. Judgment must be made.
+Equality judgment naturally has its limits, but the judgments that are possible at present and their methods are as follows.
+
+* Addition/multiplication symmetry:
+
+  `n+m == m+n`
+
+  Type variables are sorted and normalized as strings.
+
+* Equivalence of addition and multiplication, subtraction and division:
+
+  `n+n == 2*n`
+
+  Normalize to Σ[c] x == c*x, where c is a constant.
+  Constants are normalized by placing them on the left side of binary operations.
+
+* Equality of double expressions:
+
+  `n+m+l == m+n+l == l+m+n == ...`
+  `n+m*l == m*l+n`
+
+  Determined by normalizing by sorting.
+  Blocks for multiplication and division are placed to the left of addition and subtraction. Blocks are sorted by comparing the type variables on the leftmost side.
+
+* Basic inequalities:
+
+  `n > m -> m + 1 > n`
+
+* Equality:
+
+  `n >= m and m >= n -> m == n`
+
+* Transitivity of inequalities:
+
+  `n > 0 -> n > -1`
--- a/doc/EN/dev_guide/branches.md
+++ b/doc/EN/dev_guide/branches.md
@ -1,5 +1,7 @@
 # Branch naming and operation policy

+* Basically, development is done in one `main` branch (monorepo development). Create a `feature-*` branch or `issue-*` branch only when it is difficult to work without branching.
+
 ## main

 * main development branch
--- a/doc/EN/dev_guide/build_features.md
+++ b/doc/EN/dev_guide/build_features.md
@ -2,13 +2,13 @@

 ## debug

-Put into debug mode. This will log the behavior of Erg internally as it happens.
+Enter debug mode. As a result, the behavior inside Erg is sequentially displayed in the log.
 Independent of Rust's `debug_assertions` flag.

 ## japanese

 Set the system language to Japanese.
-In this build, Erg internal options, help (help, copyright, license, etc.) and error messages are guaranteed to be in Japanese.
+Erg internal options, help (help, copyright, license, etc.) and error display are guaranteed to be Japanese.

 ## simplified_chinese

@ -16,4 +16,4 @@ Set the system language to Simplified Chinese.

 ## traditional_chinese

-Set the system language to Traditional Chinese.
+Set the system language to Traditional Chinese.
--- a/doc/EN/dev_guide/directories.md
+++ b/doc/EN/dev_guide/directories.md
@ -1,24 +1,24 @@
-# Directory Structure of Erg
+# Erg repository directory structure

 ```console
- └─┬ assets: images
-   ├─ CODE_OF_CONDUCT: Code of Conduct
-   ├─┬ compiler
-   │ ├─ erg_common: common utilities
-   │ ├─ erg_compiler: Compiler
-   │ └─ erg_parser: Parser
-   ├─┬ doc
-   │ ├─┬ EN
-   │ │ ├─ API: Erg standard API
-   │ │ ├─ compiler: about implementation of the compiler
-   │ │ ├─ dev_guide: guide for developers & contributors
-   │ │ ├─ python: Knowledge of Python required for Erg development
-   │ │ ├─ syntax: syntax of Erg
-   │ │ └─ tools: about Erg's CLI tools
-   │ └─┬ JA
-   │  ...
-   ├─ examples: sample code
-   ├─ library: Erg libraries
-   ├─ src: main.rs & driver
-   └─ tests: test code
-```
+  └─┬ assets: images, etc.
+    ├─ CODE_OF_CONDUCT: Code of Conduct
+    ├─┬ compiler
+    │ ├─ erg_common: common utility
+    │ ├─ erg_compiler
+    │ └─ erg_parser: Parser
+    ├─┬doc
+    │ ├─┬ EN
+    │ │ ├─ API: Erg standard API
+    │ │ ├─ compiler: About compiler implementation
+    │ │ ├─ dev_guide: Guide for developers and contributors
+    │ │ ├─ python: Python knowledge required for Erg development
+    │ │ ├─ syntax: Erg syntax
+    │ │ └─ tools: Erg command line tools
+    │ └─┬ JA
+    │ ...
+    ├─ examples: sample code
+    ├─ library: Erg script library
+    ├─ src: directory where main.rs and driver are placed
+    └─ tests: test code
+```
--- a/doc/EN/dev_guide/doc_guideline.md
+++ b/doc/EN/dev_guide/doc_guideline.md
@ -2,10 +2,12 @@

 Any document that does not follow the rules below is subject to correction.

+* Write code comments or internal documentation in a certain tone.
+* Documents to be shown to the outside (general users) should be written more and more.
 * Always include definitions, meanings, or links to terms that appear for the first time in the document.
-* Use parentheses as a proviso only for sentences that are supplementary but necessary for understanding the main text, and use footnotes for sentences that are not essential for understanding the main text[<sup id="f1">1</sup>](#1).
-* If the document is out-of-date, follow [these instructions](https://github.com/erg-lang/erg/issues/48#issuecomment-1218247362) to update it.
+* Use parentheses as a proviso only for sentences that are supplementary but necessary for understanding the main text, and use footnotes for sentences that are not essential for understanding the main text[<sup id="f1">1</ sup>](#1).
+* If the content of the document is outdated, update it according to [this method](https://github.com/erg-lang/erg/issues/48#issuecomment-1218247362).

 ---

-<span id="1" style="font-size:x-small"><sup>1</sup> See this for how to write footnotes. [↩](#f1)</span>
+<span id="1" style="font-size:x-small"><sup>1</sup> See this for how to write footnotes. [↩](#f1)</span>
--- a/doc/EN/dev_guide/env.md
+++ b/doc/EN/dev_guide/env.md
@ -1,19 +1,19 @@
-# Development Environment
+# Development environment

-## Need to install
+## What you need to install

 * Rust (installed with rustup)

-  * ver >= 1.63.0
-  * 2021 edition
+   * ver >= 1.63.0
+   * 2021 edition

 * [pre-commit](https://pre-commit.com/)

 * Python3 interpreter

-## Recommended
+## Recommendation

 * Editor: Visual Studio Code
-* VSCode Extensions: Rust-analyzer, GitLens, Git Graph, GitHub Pull Requests and Issues, Markdown All in One, markdownlint
-* OS: Windows 10/11 | Ubuntu 20.04/22.04 | MacOS Monterey
-* Others: pyenv, mold
+* VSCode extensions: Rust-analyzer, GitLens, Git Graph, GitHub Pull Requests and Issues, Markdown All in One, markdownlint
+* OS: Windows 10/11 | Ubuntu 20.04/22.04 | Mac OS Monterey
+* Others: pyenv, mold
--- a/doc/EN/dev_guide/faq_syntax.md
+++ b/doc/EN/dev_guide/faq_syntax.md
@ -1,112 +1,116 @@
 # Erg design's "Why" and Answers

-## Why do Erg's have an ownership system but also coexist with the reference counting system?
+## Why coexist with GC when we have an ownership system?

-This is because Erg's motivation for introducing an ownership system is not for "memory management that does not rely on GC" like Rust.
-To begin with, Erg is currently a language that is transpiled into Python bytecode, so GC is used after all.
-Erg's aim in introducing the ownership system is "localization of mutable state"; in Erg, mutable objects have the concept of ownership.
-This is because shared mutable state can easily become a breeding ground for bugs and even violates type safety (see [here](./syntax/type/advanced/shared.md#SharedReference).
+Erg's motivation for introducing an ownership system is not for "memory management without relying on GC" like Rust.
+In the first place, Erg is currently a language that is reduced to Python bytecode, so GC is used after all.
+The aim of Erg's ownership system is ``localization of mutable state''. Erg has a notion of ownership attached to mutable objects.
+This is because shared mutable state is prone to bugs and even violates type safety (see [here](../syntax/type/advanced/shared.md#SharedReference)). It's a judgmental decision.

-## Why are the parentheses surrounding type parameters || instead of <> or []?
+## Why are the braces around type parameters || instead of <> or []?

-Because `<>` and `[]` cause syntax conflicts.
+This is because `<>` and `[]` cause syntax conflicts.

-```erg
+``` erg
+# version []
 id[T: Type] [t]: [T] = t
-y = id[Int] # is this a function or array accessing?
-
+y = id[Int] # is this a function?
+# <> version
 id<T: Type> {t: T} = t
-y = (id < Int, 1 > 1) # is this a tuple of bools or a call?
-
-id{T: Type} {t: T} = t # conflicts with record pattern
-y = id{Int}
-
+y = (id<Int, 1> 1) # Is this a tuple?
+# {} version
+id {T: Type} {t: T} = t
+y = id{Int} # is this a function?
+# || version
 id|T: Type| t: T = t
 y = id|Int| # OK
 ```

-## The type of {i = 1} is {i = Int}, but in OCaml and other languages it is {i: Int}. Why did Erg adopt the former syntax?
+## The type of {i = 1} is {i = Int}, but in OCaml etc. it is {i: Int}. Why did Erg adopt the former syntax?

-Because Erg is designed to treat the type itself as a value.
+This is because Erg is designed so that the type itself can also be treated as a value.

-```erg
+``` erg
 A = [Int; 3]
 assert A[2] == Int
 T = (Int, Str)
 assert T.1 == Str
 D = {Int: Str}
-assert D[Int] == Str
+assert D[Int] == Str
 S = {.i = Int}
 assert S.i == Int
 ```

-## Are there any plans to implement macros in Erg?
+## Any plans to implement macros in Erg?

-No. Macros have four main purposes: first, they are compile-time calculations. This is the role of compile-time functions in Erg.
-The second is to delay code execution. The third is common processing, for which polymorphic functions and all-symmetric types are better solutions than macros.
-Thus, the type system in Erg takes most of the functionality of macros on its shoulders, so there is no motivation to implement it.
+Not currently. Macros have four main purposes. The first is compile-time computation. This is what compile-time functions do in Erg.
+The second is code execution delays. This can be replaced with a do block. The third is the commonality of processing, for which polycorrelation and universal types are a better solution than macros. The fourth is automatic code generation, but this is not possible in Erg because it reduces readability.
+Since the Erg type system takes over most of the functionality of macros, there is no motivation to introduce them.

-## Why is there no exception mechanism in Erg?
+## Why doesn't Erg have an exception mechanism?

-Because in many cases, error handling with the `Result` type is a better solution. The `Result` type is a common error handling technique used in many relatively new programming languages.
+Because in many cases error handling with the `Result` type is a better solution. The `Result` type is a common error handling technique used in relatively new programming languages.

-Erg allows the `?` operator allows you to write without much awareness of errors.
+In Erg, the `?` operator makes writing error-free.

-```erg
+``` erg
 read_file!() =
-    f = open!("foo.txt")? # If it fails, it returns an error immediately, so `f` is of type `File`
+    f = open!("foo.txt")? # Returns an error immediately if it fails, so f is of type File
    f.read_all!()

-# `try` procedure can be used to catch and process like an exception
+# Capturing like exceptions is also possible with the try procedure
 try!:
-    do!:
+    do!
        s = read_file!()?
-        print! s
+        print!s
    e =>
-        # Blocks to execute when an error occurs
+        # block to execute when an error occurs
        print! e
        exit 1
 ```

-When Python functions are imported, by default they are all considered to be functions with exceptions (if they are not typed manually), and their return type is of type `Result`.
-If it is known that an exception will not be sent, it is made explicit by `assert`.
+When introducing Python functions, by default they are all assumed to be functions containing exceptions, with a return type of `Result`.
+If you know it won't throw an exception, make it explicit with `assert`.
+
+Another reason Erg does not introduce an exception mechanism is that it plans to introduce features for parallel programming.
+This is because the exception mechanism is not compatible with parallel execution (it is troublesome to deal with cases such as when multiple exceptions occur due to parallel execution).

 ## Erg seems to eliminate Python features that are considered bad practice, why didn't you do away with inheritance?

-Because some classes in the Python library are designed to be inherited, and completely eliminating inheritance would cause problems in their use.
-However, in Erg, classes are `Final` by default, and multiple and multi-layer inheritance is prohibited in principle, so inheritance can be used relatively safely.
+This is because Python libraries have classes that are designed on the assumption that they will be inherited, and if inheritance is completely abolished, problems will arise in their operation.
+However, in Erg, classes are final by default and multiple/multilevel inheritance is prohibited in principle, so inheritance can be used relatively safely.

-## Why does subtype inference for polymorphic functions point to nominal traits by default?
+## Why do polymorphic subtype inferences point to nominal traits by default?

-Because pointing to structural traits by default complicates type specification and may introduce unintended behavior by the programmer.
+Pointing to structural traits by default complicates typing and can introduce behavior unintended by the programmer.

-```erg
+``` erg
 # If T is a subtype of a structural trait...
-# f: |T <: Structural Trait {.`_+_` = Self.(Self) -> Self; .`_-_` = Self.(Self) -> Self}| (T, T) -> T
+# f: |T <: Structural Trait {.`_+_` = Self.(Self) -> Self; .`_-_` = Self.(Self) -> Self}| (T, T) -> T.
 f|T| x, y: T = x + y - x
 # T is a subtype of a nominal trait
 # g: |T <: Add() and Sub()| (T, T) -> T
 g|T| x, y: T = x + y - x
 ```

-## Will Erg implement the ability to define its own operators?
+## Will Erg not implement the ability to define its own operators?

-A: There are no plans to do so. The main reason is that allowing the definition of custom operators raises the question of how to handle the concatenation order. Scala and Haskell, which allow the definition of custom operators, have different approaches, and this can be seen as evidence of a syntax that can lead to differences in interpretation. This can be seen as evidence of a syntax that can lead to differences in interpretation, and also has the disadvantage of creating code with low readability.
+A: There are no plans for that. The main reason is that allowing the definition of custom operators raises the question of what to do with their associativity. Scala and Haskell, which can define their own operators, handle them differently, but this can be seen as proof that the grammar can lead to different interpretations. Another disadvantage of custom operators is that they can create code that is not readable.

-## Why did Erg do away with augmented assignment operators like `+=`?
+## Why did Erg deprecate extended assignment operators like +=?

-First of all, variables are not mutable in Erg. In other words, reassignment is not possible. Once an object is assigned to a variable, it is bound to that variable forever until it is released out of scope. Once this is understood, the story is simple. For example, `i += 1` means `i = i + 1`, but such a construction is incorrect because variables are not reassignable. Another design principle of Erg is that operators have no side effects, and while Python generally does this, for some objects, such as Dict, the augmented assignment operator changes the internal state of the object. This is not a very beautiful design.
-That is why augmented assignment operators have been deprecated in its entirety.
+First, there is no variable mutability in Erg. In other words, it cannot be reassigned. Once an object is bound to a variable, it remains bound to that variable until it goes out of scope and is freed. Mutability in Erg means object mutability. Once you know this, the story is easy. For example, `i += 1` means `i = i + 1`, but such syntax is illegal because variables are not reassigned. Another Erg design principle is that operators should not have side effects. Python is mostly like that, but for some objects such as Dict, extended assignment operators change the internal state of the object. This is not a very beautiful design.
+That's why extended assignment operators are obsolete altogether.

-## Why does Erg give special grammatical treatment to objects with side effects?
+## Why does Erg syntactically specialize objects with side effects?

-Localization of side effects is an important part of code maintainability.
+Localizing side effects is an important aspect of code maintainability.

-However, there are certainly ways to avoid giving side effects special linguistic treatment. For example, procedures can be substituted with algebraic effects (features on the type system).
-But such congruence is not always correct. For example, Haskell did not treat strings as special, just arrays of characters, but this abstraction was wrong.
+But there is certainly a way to get around side effects without linguistic specialization. For example, procedures can be substituted with algebraic effects (functions on the type system).
+But such a union is not always correct. For example, Haskell treats strings as just arrays of characters without special treatment, but this abstraction is wrong.

-In what cases can we say that unification was wrong? One indicator is "does the congruence make the error message difficult to read?
-The Erg designers decided that the error messages would be easier to read if side effects were treated specially.
+In what cases could it be said that union was wrong? One indicator is "whether the unification makes the error message less readable".
+The Erg designers decided that giving special treatment to side effects would make error messages easier to read.

-Erg has a powerful type system, but it does not dominate everything with types.
-If it did, it would end up the same way as Java, which tried to dominate everything with classes.
+Erg has a strong type system, but types don't rule everything.
+If you do, you'll end up with the same fate that Java tried to rule everything with classes.
--- a/doc/EN/dev_guide/i18n_messages.md
+++ b/doc/EN/dev_guide/i18n_messages.md
@ -1,59 +1,58 @@
 # Multilingualization of Messages

-Erg is working on making all messages (start, option, doc, hint, warning, error messages, etc.) multilingual within the language.
-This project is open to anyone without detailed knowledge of Rust or Erg. Your participation is always welcome.
+Erg is making its messages (start, options, documentation, hints, warnings, error messages, etc.) multilingual.
+You don't need detailed knowledge of Rust or Erg to participate in this project. We appreciate your cooperation.

-Here is how to translate them.
+The method for multilingualization is explained below.

-## Search `switch_lang!`
+## Look for `switch_lang!`

-In the Erg source code, look for the item `switch_lang!` (use grep or your editor's search function).
+Find the entry `switch_lang!` in the Erg source code (use grep or your editor's search function).
 You should find something like this:

 ```rust
 switch_lang!(
-    "japanese" => format!("この機能({name})はまだ正式に提供されていません"),
+    "japanese" => format!("This feature ({name}) is not officially available yet"),
    "english" => format!("this feature({name}) is not implemented yet"),
 ),
 ```

-This message is currently supported only in Japanese and English. Let's add a simplified Chinese message as a test.
+This message is currently supported in Japanese and English only. Let's try adding a simplified Chinese message.

-## Add a New Message
+## add a message

-Add translated messages as you see the content in other languages. Don't forget the comma (`,`) last.
+Add translated messages while viewing content in other languages. Don't forget the comma (`,`) at the end.

 ```rust
 switch_lang!(
-    "japanese" => format!("この機能({name})はまだ正式に提供されていません"),
-    "simplified_chinese" => format!("该功能({name})还没有正式提供"),
+    "japanese" => format!("This feature ({name}) is not officially available yet"),
+    "simplified_chinese" => format!("This function ({name}) has been officially provided"),
    "english" => format!("this feature({name}) is not implemented yet"),
 ),
 ```

-Note that English is the default and must come last.
-The `{name}` part is a Rust formatting feature that allows you to embed the contents of a variable (`name`) into a string.
+Note that English is the default and should always come last.
+The `{name}` part is Rust's formatting feature that allows you to embed the contents of a variable (`name`) into a string.

 ## Build

-Now, let's build with the `--features simplified_chinese` option.
+Now let's build with the `--features simplified_chinese` option.

 <img src="../../../assets/screenshot_i18n_messages.png" alt='screenshot_i18n_messages'>

-We did it!
+You did it, did not you!

-## FAQ
+## FAQs

 Q: What does a specification like `{RED}{foo}{RESET}` mean?
-A: {RED} and subsequent letters will be displayed in red. {RESET} will restore the color.
+A: Everything after {RED} is displayed in red. {RESET} restores the color.

-Q: If I want to add my language, how do I replace the `"simplified_chinese" =>` part?
-
-The following languages are currently supported:
+Q: If I want to add my own language, how do I replace the `"simplified_chinese" =>` part?
+A: We currently support the following languages:

 * "english" (default)
-* "japanese"
-* "simplified_chinese"
-* "traditional_chinese"
+* "japanese" (Japanese)
+* "simplified_chinese" (Simplified Chinese)
+* "traditional_chinese" (Traditional Chinese)

-If you would like to add languages other than these, please make a request.
+If you would like to add languages other than these, please make a request.
--- a/doc/EN/dev_guide/rust_code_guideline.md
+++ b/doc/EN/dev_guide/rust_code_guideline.md
@ -1,23 +1,23 @@
 # Guidelines for Rust code

-## Local rules
+## local rules

-* Use `log!` for debugging output (use `println!` etc. for output processing required for release).
-* Unused or internal variables and methods (private and used only for specific functions) should be prefixed with `_`. To avoid conflicts with reserved words, add one trailing `_`.
+* Use `log!` for output for debugging (use `println!` etc. for output processing that is also necessary for release).
+* Unused or internal variables/methods (private and used only for specific functions) must be prefixed with `_`. If you want to avoid conflicts with reserved words, add one `_` to the end.

-## Encouraged code
+## Recommended code

-* Define and use domain-specific Enums instead of numeric enumerations or bool.
-* Minimize access modifiers. Use `pub(mod)` or `pub(crate)` in preference even when publishing.
-* Explicitly convert iterable objects in for expressions to iterators (`for i in x.iter()` instead of `for i in x`).
-* Evaluate Lazily. For example, use `unwrap_or_else` instead of `unwrap_or` if `default` is not a literal.
+* Define and use domain-specific Enums instead of numeric enumerations or bools.
+* Keep access modifiers to a minimum. Prioritize using `pub(mod)` or `pub(crate)` even when publishing.
+* Convert an iterable object in a for expression explicitly to an iterator (`for i in x.iter()` instead of `for i in x`).
+* Lazy evaluation. For example, if `default` is non-literal, use `unwrap_or_else` instead of `unwrap_or`.

-## Unsolicited code
+## Code not encouraged

-* Use return-type overloading a lot. Specifically, code that uses non-trivial `.into` too often. This is because the result of type inference may be counter-intuitive. In this case, it is recommended to use `from` instead.
-* Use `Deref` a lot. This causes practically the same problem as inheritance.
+* Make heavy use of return type overloading. Specifically code that uses a lot of non-obvious `.into`. This is because type inference results can be counter-intuitive. In this case it is recommended to use `from` instead.
+* Make heavy use of `Deref`. This effectively poses the same problem as inheritance.

-## Code that changes its decision depending on the context
+## Code that makes decisions based on context

 * Define unused helper methods.
-* Uses `unwrap`, `clone`. In some cases, there is no choice but to do so.
+* Use `unwrap` and `clone` a lot. In some cases there is nothing better than doing so.
--- a/doc/EN/dev_guide/terms.md
+++ b/doc/EN/dev_guide/terms.md
@ -1,10 +1,13 @@
-# Dictionary of Terminology
+# Glossary

 ## symbol

 ### &excl;

-### [&#35;](../syntax/00_basic.md/#comments)
+A marker added to the end of an identifier to indicate that it is a procedure or variable type.
+Or the mutating operator.
+
+### [&#35;](../syntax/00_basic.md/# comment)

 ### $

@ -144,7 +147,7 @@

 ## L

-### let-polymorphism -> [rank1 polymorphism]
+### let-polymorphism -> [rank 1 polymorphism]

 ### [log]

@ -206,7 +209,7 @@

 ## T

-### Trait
+### Traits

 ### [True]

@ -227,3 +230,610 @@
 ## Y

 ## Z
+
+## A line
+
+### [Assertion]
+
+To check (typically at runtime) whether a condition is true in code. This is done using the `assert` function, etc.
+
+``` erg
+sum = !0
+for! 0..10, i =>
+    sum.add!i
+
+assert sum == 55
+```
+
+### Value Object
+
+In Erg, equivalent to base object. It can be evaluated at compile time and has a trivial comparison method.
+
+### [Attachment patch](../syntax/29_decorator.md#attach)
+
+A patch that gives the trait a standard implementation.
+
+### Ad hoc polymorphism -> [No overloading](../syntax/type/overloading.md)
+
+Polymorphism with so-called overloading.
+
+### Attribute -> [attribute]
+
+The `y` part in the `x.y` identifier.
+
+### Arity
+
+How many operands the operator takes.
+
+### [Dependent type](../syntax/type/dependent_type.md)
+
+A type whose argument is a value (idiomatically, not a type).
+
+### immutable -> [immutable]
+
+Indicates that the target will not change.
+Variables in other languages are also immutable/mutable, but in Erg all variables are immutable.
+
+### arguments -> [arguments]
+
+### instance
+
+An object created by a class. An element of class type.
+
+### [instant block](../syntax/00_basic.md#expression separator)
+
+``` erg
+x =
+    y = f(a)
+    z = g(b,c)
+    y+z
+```
+
+### index
+
+of the form `x[i]`, or the `i` part thereof. We call `x` an Indexable object.
+
+### [indent](../syntax/00_basic.md#indent)
+
+Align text to the right by moving toward spaces. Indentation.
+Ergs represent blocks by indentation. This is called the offside rule.
+
+### Aliases
+
+Alias.
+
+### error
+
+Abnormal conditions defined in the specification.
+
+* [Error handling]
+
+### [operator](../syntax/06_operator.md)
+
+An object that applies an operation to its operands. or a symbol denoting that object.
+
+* [operator binding strength]
+
+### Override
+
+Overriding superclass methods in subclasses.
+In Erg you have to add `Override` decorator when overriding.
+
+### [No overloading](../syntax/type/overloading.md)
+
+### Offside rule -> [indent](../syntax/00_basic.md#indent)
+
+### [object]
+
+* Object-orientation
+
+### operand -> [operand](../syntax/06_operator.md)
+
+### operator -> [operator](../syntax/06_operator.md)
+
+## Ka line
+
+### [kind](../syntax/type/advanced/kind.md)
+
+Types of so-called types.
+
+### [visibility]
+
+The property of whether an identifier can be referenced externally (out of scope, or in another module or package).
+
+### [type]
+
+An object that groups terms.
+
+* [type specification]
+* [type erasure](../syntax/type/advanced/erasure.md)
+* [type inference]
+* [type annotation](../syntax/type/conv_type.md)
+* [type argument]
+* [type addition](../syntax/type/advanced/erasure.md)
+* [type variable](../syntax/type/type_variable.md)
+* [type constraint]
+
+### [Guard]
+
+### Encapsulation
+
+Hiding implementation details.
+
+### [variable]
+
+Must not be immutable.
+
+* [mutable object]
+* [variable]
+* [variable reference]
+* [variable array]
+* [variable arguments]
+
+### [function](../syntax/04_function.md)
+
+A subroutine with no side effects.
+
+* [Functional programming](../syntax/23_scope.md#Avoiding mutable stateFunctional programming)
+
+### base type
+
+### nominative
+
+Distinguish by name rather than by symmetrical structure.
+
+* [named type] -> [class](../syntax/type/04_class.md)
+* [Annunciation]
+* [nominal subtype](../syntax/type/05_nst_vs_sst.md)
+
+### capture -> [closure]
+
+### [covariant]
+
+In Erg, if `T <: U` then `K(T) <: K(U)` then `K` is said to be covariant.
+
+### [keyword arguments]
+
+`k` in the form of function call `f(k: v)`. You can specify actual arguments by formal argument name instead of by order.
+
+### empty set -> [{}]
+
+### section
+
+* [Interval type](../syntax/type/11_interval.md)
+* interval operator
+
+### Embedded
+
+Erg standard APIs not implemented in .er files.
+
+### [class](../syntax/type/04_class.md)
+
+Structure/abstract data type with inheritance function. In Erg, it is a type to implement named subtyping and overriding.
+In Erg, modules are the responsibility of module objects, and types are the type object, while other languages may be responsible for modules and types.
+
+### [Closure]
+
+### [global variables]
+
+### [Clone]
+
+### [inheritance](../syntax/type/07_inheritance.md)
+
+To define a class that is a superset of another class.
+The class that inherits is called the superclass, and the class that inherits is called the subclass.
+A subclass has all the functionality of its superclass.
+
+### high floor
+
+* [higher-order kind](../syntax/type/advanced/kind.md)
+* higher order type
+* Higher-order functions
+
+### [public variables]
+
+### [structural subtype]
+
+### ~~back reference~~ -> [back reference]
+
+### [copy]
+
+### comment
+
+### [Collection](../syntax/10_array.md)
+
+### Colon -> [:]
+
+### [constructor](../syntax/type/04_class.md)
+
+### container
+
+### Compiler
+
+### [compile-time computation](../syntax/04_function.md#compile-time function)
+
+### comma -> [,]
+
+## sa line
+
+### recursion
+
+Refer to yourself.
+
+* recursive
+* [Recursive function](../syntax/04_function.md#Recursive function)
+
+### subscript -> [index]
+
+### [subtyping polymorphism](../syntax/type/overloading.md)
+
+Polymorphism with subtyping. Subtyping corresponds to set containment in types.
+
+### Subroutine
+
+An object that modularizes processing. A generic term for functions, procedures, and methods in Erg.
+
+### [reference](../syntax/18_memory_management.md#borrowed)
+
+* reference object
+* [Reference counting (RC)](../syntax/18_memory_management.md#memory management)
+* Reference equality -> [side effect](../syntax/07_side_effect.md)
+
+### [identifier](../syntax/02_variable.md/# assignment)
+
+### signature
+
+* type signature
+
+### [dict](../syntax/11_dict.md)
+
+### [natural number] -> [Nat]
+
+### Generics -> [Generic]
+
+### Generator
+
+### [projective type]
+
+### borrow -> [reference](../syntax/18_memory_management.md#borrowed)
+
+### [shadowing](../syntax/02_name.md# variables)
+
+To override a reference to a variable by defining a variable with the same name in an inner scope.
+
+### kind -> [kind](../syntax/type/advanced/kind.md)
+
+Roughly the type of type.
+
+### [set] -> [set]
+
+In Erg, it means a Set object.
+
+### Predicate
+
+* [predicate function]
+
+A function that returns a bool type.
+
+### Conditional branch
+
+### [Ownership]
+
+The concept of object uniqueness.
+If you have ownership of an object, you can take a mutable reference to it.
+
+### Boolean -> [Bool]
+
+### Singleton
+
+An instance created from a class that can create only one instance. A design pattern that ensures that only one instance of a class is created.
+
+### [Symbol] -> [Identifier](../syntax/02_name.md)
+
+* [symbolization]
+
+### [script](../syntax/00_basic.md# script)
+
+A file containing an Erg program.
+
+### Scope
+
+Units in variable management. An outer scope cannot refer to a variable that exists in an inner scope.
+Objects with a reference count of 0 are freed when the scope exits.
+
+### spread operator -> [expansion assignment]
+
+### [slice](../syntax/10_array.md#slice)
+
+An object representing a subsequence of the array, generated in the form `x[a..b]`.
+
+### control characters
+
+### [Integer] -> [Int]
+
+A set of natural numbers plus negative numbers.
+
+### [set](../syntax/12_set.md)
+
+### Semicolon -> [;]
+
+### [Declaration](../syntax/03_declaration.md)
+
+Explicitly type variables.
+
+### Full name
+
+* universal type -> [polymorphic type](../syntax/type/quantified.md)
+  * closed universal
+  * Open Universal
+* universal function -> polycorrelation function
+* universal quantification
+
+### prefix operator
+
+Operator `∘` applied in the form `∘x`.
+
+### mutual recursion
+
+### subscript -> [index]
+
+### [attributes]
+
+* [attribute subtype]
+
+## Ta line
+
+### [algebra](../syntax/02_name.md)
+
+* [algebraic type](../syntax/type/13_algebraic.md)
+* algebraic data types
+
+### [assignment](../syntax/02_variable.md/#assignment)
+
+### Multiple
+
+* [Multiple inheritance](../syntax/type/07_inheritance.md/#Prohibition of multiple inheritance)
+* Multiple assignment
+* Overload -> [No overloading]
+
+### Polymorphism
+
+* [polymorphic type](../syntax/type/quantified.md)
+* polycorrelation coefficient
+
+### polymorphism -> [polymorphism]
+
+### duck typing
+
+### [tuple](../syntax/11_tuple.md)
+
+### Single-phase
+
+* Single phase
+* Single-phase type
+* Single correlation coefficient
+
+### [Lazy initialization]
+
+### Extraction Assignment
+
+### Abstract syntax tree -> [AST]
+
+### Infix operator
+
+The operator `∘` applied in the form `x∘y`.
+
+### [constant](../syntax/02_name.md/#constant)
+
+Immutable, compile-time evaluable algebra.
+
+* [constant type](../syntax/type/advanced/const.md)
+* [constant expression](../syntax/type/advanced/const.md)
+
+### [definition]
+
+Allocating an object corresponding to a variable.
+
+### Provided Attributes
+
+Attributes available as API. Especially attributes auto-implemented by traits.
+
+### [Apply]
+
+To pass an argument to a function object and get the evaluation result.
+
+### [decorator](../syntax/29_decorator.md)
+
+``` erg
+@deco
+f x = ...
+```
+
+syntactic sugar, or `deco`. Roughly equal to `_f x = ...; f = deco _f`. `deco` itself is just a higher-order subroutine.
+
+### destructor
+
+Method called when the object is destroyed.
+
+### procedure -> [procedure](../syntax/08_procedure.md)
+
+A subroutine that reads and writes mutable state.
+It is sometimes said that the execution result of a program can change depending on the order in which the procedures are called, but this is incorrect if we are talking about commutativity.
+For example, operators that are subtypes of functions are generally not commutative.
+
+### [default arguments](../syntax/04_function.md/#default arguments default-parameters)
+
+A function that allows you to omit the specification of actual arguments at the time of calling by specifying default values for formal arguments.
+
+### Expand
+
+* [expansion operator]
+* [expansion assignment]
+
+### [special format](../syntax/../API/special.md)
+
+An object that cannot be passed as an actual argument.
+
+### anonymous function -> [anonymous function](../syntax/20_lambda.md)
+
+A function object created by the anonymous function operator `->`. Can be used without defining a name.
+
+### dot operator (`.`) -> [attribute reference]
+
+### Top
+
+* Top type -> [Structural Object]
+* Top class -> [Object]
+
+### [trait](../syntax/type/03_trait.md)
+
+## na line
+
+### [Comprehension](../syntax/27_comprehension.md)
+
+### ~~Infix operator~~ -> [Infix operator]
+
+### [namespace]
+
+## is a line
+
+### [Array](../syntax/10_array.md)
+
+### [derived type](../syntax/type/variances.md/# user-defined type variations)
+
+### [pattern (match)](../syntax/26_pattern_matching.md)
+
+### [package](../syntax/33_package_system.md)
+
+### hashmap -> [dict](../syntax/11_dict.md)
+
+### [patch](../syntax/type/07_patch.md)
+
+### public variables -> [public variables](../syntax/19_visibility.md)
+
+### parameter -> [argument](../syntax/04_function.md)
+
+### [Parametric Polymorphism](../syntax/type/overloading.md)
+
+### [contravariant](../syntax/type/advanced/variance.md)
+
+### Compare
+
+* [comparison operator]
+* [comparable type]
+
+### [private variable](../syntax/19_visibility.md)
+
+### standard
+
+* standard output
+* standard input
+* standard library
+
+### [side effects](../syntax/07_side_effect.md)
+
+Code should/not read/write external mutable state.
+
+### complex number -> [Complex]
+
+### [Float] -> [Float]
+
+### private variables -> [private variables]
+
+### Boolean algebra -> [Bool]
+
+### [procedure](../syntax/08_procedure.md)
+
+### [arguments](../syntax/04_function.md)
+
+### Partial Typing -> [Subtyping]
+
+### [immutable]
+
+In Erg, an object should never change its contents.
+
+* [immutable object]
+* [immutable type]
+* [immutable reference]
+
+### [sieve type](../syntax/type/12_refinement.md)
+
+### [block]
+
+### Destructuring assignment
+
+### [variable](../syntax/02_variable.md)
+
+### bottom
+
+* bottom type -> [{}]
+* Bottom class -> [Never]
+
+### [Polymorphism]
+
+## ma line
+
+### ~~ prefix operator ~~ -> prefix operator
+
+### [marker type](../syntax/type/advanced/marker_trait.md)
+
+### [anonymous function](../syntax/21_lambda.md)
+
+### mutable -> [mutable]
+
+### [move]
+
+### methods
+
+### Metacharacters
+
+### [module](../syntax/24_module.md)
+
+### [String] -> [Str]
+
+* [String interpolation](../syntax/01_literal.md/#Str literal)
+
+### Return value
+
+## or line
+
+### [phantom type](../syntax/type/advanced/phantom.md)
+
+### Request Attributes
+
+### [element]
+
+### [call]
+
+## Ra line
+
+### [Library]
+
+### lambda expression -> [anonymous function](../syntax/20_lambda.md)
+
+### rank
+
+* [rank2 polymorphism](../syntax/type/advanced/rank2type.md)
+
+### [literal](../syntax/01_literal.md)
+
+* [literal identifier](../syntax/18_naming_rule.md/#literal identifier)
+
+### [quantified](../syntax/type/quantified.md)
+
+### [Layout](../syntax/type/mut.md)
+
+### [enum](../syntax/type/10_enum.md)
+
+### [record](../syntax/12_record.md)
+
+* [record type]
+* Record Polymorphism -> [Column Polymorphism]
+
+### [column polymorphism]
+
+### [local variables](../syntax/19_visibility.md)
+
+## line
+
+### Wildcard
--- a/doc/EN/dev_guide/unify_terms.md
+++ b/doc/EN/dev_guide/unify_terms.md
@ -0,0 +1,88 @@
+# Unification of terminology
+
+## Accessibility, Visibility
+
+Use Visibility.
+
+## Complement (negative type, complementary type)
+
+Use negative types. The result of Complement is not necessarily Not type.
+
+## Diff (difference type, exclusion type, direct difference type)
+
+Use exclusion types. The result of Diff is not always Not type.
+
+## Intersection (intersection type, intersection type, Cartesian product type)
+
+Use intersection types. Do not use Cartesian product types. This is because there is also a usage that regards a tuple as a Cartesian product type.
+However, from the point of view of attribute subtyping, it is essentially equivalent to Erg's And type.
+Also, the result of Intersection is not necessarily And type. For example `{1, 2, 3} and {1, 2} == {1, 2}`.
+
+## Translation of Nominal subtyping
+
+There are nominal/nominal/nominal subtyping, but use nominal subtyping.
+
+## Ratio type translation
+
+Use rational numbers. Since Float is provided separately, it is not called a floating-point number type.
+
+## Union
+
+Use a union type. The result of Union is not necessarily Or type.
+
+## Type bound, Type constraint
+
+A list of predicate expressions given to quantified and sieve types. Use type bounds.
+
+## subroutines, routines, subprograms
+
+Use subroutines.
+
+## Referentially transparent/not, with/without side effects
+
+Use with/without side effects.
+
+## identifiers, algebra, variables, names, symbols
+
+In its original meaning,
+
+* Symbol: Characters (except symbols, control characters, etc.) that are solid-written in source code that are not string objects (not enclosed in ""). Symbols exist as primitive types in Ruby, Lisp, etc., but they are not treated as objects in Erg.
+* Identifier: A symbol that (and can) refer to some object, not a reserved word. For example, in Python class and def cannot be used as identifiers. Since Erg has no reserved words, all symbols can be used as identifiers except some symbols.
+* Name: Almost same meaning as identifier. It is sometimes used synonymously with algebra in Erg.
+* Algebra name: equivalent to identifier in Erg. In C, function names are identifiers, not algebraic names. "Algebra" refers to the language feature itself that allows you to assign objects with `=` (variable assignment operator) or `=` (constant assignment operator).
+
+``` erg
+algebraic name <: (name == identifier) <: symbol
+variable + constant == algebra
+```
+
+However, what should be called "algebra" is often called "variable". This is the effect of mathematical terminology.
+A variable whose value content can change is a mutable variable, and a variable whose value content does not change is an immutable variable.
+Note that constants are always immutable.
+
+Algebraic names and names are not used in Erg, and uniform identifiers are used.
+However, in general, `v` with `v = 1` is called "Variable v", and `C` with `C = 1` is called "Constant C". .
+
+## Attribute, Field, Property
+
+Attribute, use attributes.
+By the way, a record is a function that can define an object with element attributes without a class.
+
+## Application, Call
+
+Giving arguments to a subroutine object and getting a result.
+Use Call. This is because Application has a usage of "applied software".
+
+## Array, List
+
+Use Arrays. Erg arrays are (generally) contiguous in memory.
+List refers to a so-called linked list, or a list as a Python data type.
+
+## procedures, procedures
+
+Standardize on procedures. Subroutine is a generic term for functions (and operators), procedures and methods. Callable is also anything that implements `__call__`.
+
+## lambda functions, lambda expressions, anonymous functions, anonymous functions
+
+Unify with anonymous functions. In English, Lambda can be used to shorten the number of characters, but the official name is Anonymous function.
+Also, Erg's anonymous functions are not anonymous, so we don't use them.
--- a/doc/EN/migration_from_py.md
+++ b/doc/EN/migration_from_py.md
@ -1,28 +1,25 @@
-# Tips on migrating from Python to Erg
+# Tips for migrating from Python to Erg

-## Want to convert a string to an int, etc
+## I want to convert a string to int etc.

 Use the `parse` method of the `Str` class. It returns a `Result` type.

 ```python
-# Python
 s: str
 i: int = int(s)
 ```

-```erg
-# Erg
+``` erg
 s: Str
-res: Result(Int, IntParseError) = s.parse Int
+res: Result(Int, IntParseError) = s. parse Int
 i: Int = res.unwrap()
-f: Result(Float, FloatParseError) = s.parse Float
+f: Result(Float, FloatParseError) = s. parse Float
 ```

 You can also use the `try_from` method.

-```erg
-# Erg
+``` erg
 s: Str
 i: Int = Int.try_from(s).unwrap()
 f: Float = Float.try_from(s).unwrap()
-```
+```
--- a/doc/EN/python/bytecode_instructions.md
+++ b/doc/EN/python/bytecode_instructions.md
@ -1,7 +1,7 @@
 # Python Bytecode Instructions

-Python bytecode variable manipulation instructions are accessed through namei (name index). This is to realize Python's dynamic variable access (access by string using eval, etc.).
-Each instruction is 2 bytes, and instructions and arguments are stored in a little endian.
+Python bytecode variable manipulation commands are accessed through namei (name index). This is to achieve dynamic variable access in Python (which can be accessed as a string using eval, etc.).
+One instruction is 2 bytes, and the instruction and arguments are stored in little endian.
 Instructions that do not take arguments also use 2 bytes (the argument part is 0).

 ## STORE_NAME(namei)
@ -16,7 +16,7 @@ globals[namei] = stack.pop()
 stack.push(globals[namei])
 ```

-Only called at the top level.
+Only called at top level.

 ## LOAD_GLOBAL(namei)

@ -24,7 +24,7 @@ Only called at the top level.
 stack.push(globals[namei])
 ```

-To Load what was STORE_NAME at the top level in the inner scope, but namei at the top level is not necessarily the same as namei in a code object of a certain scope (namei, not name, is the same).
+It is for loading STORE_NAME at the top level in the inner scope, but `namei` at the top level is not necessarily the same as namei in the code object of a certain scope (name is the same, not namei)

 ## LOAD_CONST(namei)

@ -32,10 +32,10 @@ To Load what was STORE_NAME at the top level in the inner scope, but namei at th
 stack.push(consts[namei])
 ```

-Load constants in the constants table.
-Currently (Python 3.9), CPython MAKE_FUNCTION every time a lambda function is called "\<lambda\>".
+Load constants in the constant table.
+Currently (Python 3.9), in CPython, each lambda function is MAKE_FUNCTION with the name "\<lambda\>"

-````console
+```console
 >>> dis.dis("[1,2,3].map(lambda x: x+1)")
 1 0 LOAD_CONST 0 (1)
        2 LOAD_CONST 1 (2)
@ -47,33 +47,30 @@ Currently (Python 3.9), CPython MAKE_FUNCTION every time a lambda function is ca
        14 MAKE_FUNCTION 0
        16 CALL_FUNCTION 1
        18 RETURN_VALUE
-````
+```

 ## STORE_FAST(namei)

-```python
 fastlocals[namei] = stack.pop()
-```
-
-Probably corresponds to STORE_NAME at the top level.
-This is supposed to store an unreferenced (or single) variable.
-Is it for optimization that the global space has its own instruction?
+Possibly corresponds to STORE_NAME at top level
+The unreferenced (or single) variable is assumed to be stored by this
+Is it for optimization that the global space has its own instructions?

 ## LOAD_FAST(namei)

 stack.push(fastlocals[namei])
-fastlocals is varnames?
+fastlocals are varnames?

 ## LOAD_CLOSURE(namei)

 ```python
 cell = freevars[namei]
-stack.push(cell)
+stack. push(cell)
 ```

-After that BUILD_TUPLE is called.
-It is only called in a closure, and cellvars is supposed to store references in the closure.
-Unlike LOAD_DEREF, the entire cell (container with references) is pushed onto the stack
+Then BUILD_TUPLE is called
+It is only called inside the closure, and cellvars are supposed to store references inside the closure.
+Unlike LOAD_DEREF, each cell (container filled with references) is pushed to the stack

 ## STORE_DEREF(namei)

@ -82,8 +79,8 @@ cell = freevars[namei]
 cell.set(stack.pop())
 ```

-Variables without references in the inner scope are STORE_FAST, but referenced variables are STORE_DEREF.
-In Python, the reference count is increased or decreased within this instruction
+Variables without references in inner scopes are STORE_FAST, but referenced variables are STORE_DEREF
+In Python, the reference count is incremented and decremented within this instruction

 ## LOAD_DEREF(namei)

@ -92,26 +89,26 @@ cell = freevars[namei]
 stack.push(cell.get())
 ```

-## Name List
+## name list

 ### varnames

-List of names of internal variables of the function corresponding to `fast_locals`.
-Even if there is a variable with the same name in names, it is not basically the same (it is newly created, and the outside variable cannot be accessed from its scope).
-In other words, variables defined in scope without external references go into varnames
+Name list of function internal variables corresponding to fast_locals
+Even if there are variables with the same name in names, they are basically not the same (newly created and outside variables cannot be accessed from that scope)
+i.e. variables without external references defined in scope go into varnames

 ### names

-Corresponding to `globals`.
-A list of names of external constants (reference only) used in a scope (even ordinary variables at the top level go into names).
-In other words, constants defined outside the scope go into names
+Compatible with globals
+Name list of external constants (only referenced) used within the scope (at the top level, even ordinary variables are included in names)
+i.e. constants defined outside the scope go into names

-## free variable
+## free variables

-Corresponds to `freevars`.
-Variables captured by closure. It behaves static within the same function instance.
+Compatible with freevars
+Variables captured by the closure. It behaves statically within the same function instance.

 ## cell variables

-Corresponds to `cellvars`.
-Variables captured by an inner closure function within a function. A copy is made, so the original variable remains intact.
+Corresponds to cellvars
+Variables captured within a function to an inner closure function. Since a copy is made, the original variable remains as it is.
--- a/doc/EN/syntax/14_set.md
+++ b/doc/EN/syntax/14_set.md
@ -1,16 +1,16 @@
 # Set

-A set is an unordered array with no duplicates.
+A set represents a collection, which is structurally a duplicate, unordered array.

-```erg
+``` erg
 assert Set.from([1, 2, 3, 2, 1]) == {1, 2, 3}
 assert {1, 2} == {1, 1, 2} # duplicates are automatically removed
 assert {1, 2} == {2, 1}
 ```

-Sets can perform mathematical set operations.
+Sets can perform set operations.

-```erg
+``` erg
 assert 1 in {1, 2, 3}
 assert not 1 in {}
 assert {1} or {2} == {1, 2}
@ -18,30 +18,29 @@ assert {1, 2} and {2, 3} == {2}
 assert {1, 2} not {2} == {1}
 ```

-A set is a homogenous collection. Objects of different classes must be made equal in order to coexist.
+A set is a homogeneous collection. In order for objects of different classes to coexist, they must be homogenized.

-```erg
-s1 = {"a", 1, "b", -1} # TypeError
-s2: {Int or Str} = {"a", 1, "b", -1}
+``` erg
+s: {Int or Str} = {"a", 1, "b", -1}
 ```

-## Set as Type
+## Sets as types

-Sets can also be treated as types. Such a type is called an __Enum type_.
+Sets can also be treated as types. Such types are called __Enum types__.

-```erg
+``` erg
 i: {1, 2, 3} = 1
 assert i in {1, 2, 3}
 ```

-The elements of the set are directly the elements of the type.
-Note that the set itself is different.
+Elements of the set are directly elements of the type.
+Note that the sets themselves are different.

-```erg
+``` erg
 mut_set = {1, 2, 3}.into {Int; !3}
 mut_set.insert!(4)
 ```

 <p align='center'>
    <a href='./13_record.md'>Previous</a> | <a href='./15_type.md'>Next</a>
-</p>
+</p>
--- a/doc/EN/syntax/15_type.md
+++ b/doc/EN/syntax/15_type.md
@ -4,4 +4,4 @@ Types are a very important feature in Erg, so we have a [dedicated section](./ty

 <p align='center'>
     <a href='./14_set.md'>Previous</a> | <a href='./16_iterator.md'>Next</a>
-</p>
+</p>
--- a/doc/EN/syntax/18_ownership.md
+++ b/doc/EN/syntax/18_ownership.md
@ -1,110 +1,110 @@
-# Ownership System
+# Ownership system

-Since Erg is a language that uses Python as its host language, its method of memory management is dependent on the Python implementation.
-Semantically, however, Erg's memory management is different from that of Python. The most noticeable differences appear in the ownership system and the prohibition of circular references.
+Since Erg is a language that uses Python as the host language, the method of memory management depends on the Python implementation.
+But semantically Erg's memory management is different from Python's. A notable difference is in the ownership system and the prohibition of circular references.

 ## Ownership

-Erg has an ownership system influenced by Rust.
-While Rust's ownership system is generally considered arcane, Erg's has been simplified to make it intuitive.
-In Erg, ownership is attached to __mutable objects__, which cannot be referenced after you lose ownership.
+Erg has an ownership system inspired by Rust.
+Rust's ownership system is generally considered esoteric, but Erg's is simplified to be intuitive.
+In Erg, __mutable objects__ are owned and cannot be referenced after ownership is lost.

-```erg
-v = [1, 2, 3].into [Int; !3].
+``` erg
+v = [1, 2, 3].into [Int; !3]

-push!vec, x =
+push! vec, x =
    vec.push!(x)
-    vec.
+    vec

-# ownership of v's contents ([1, 2, 3]) is transferred to w
+# The contents of v ([1, 2, 3]) are owned by w
 w = push! v, 4
 print! v # error: v was moved
-print! w # [1, 2, 3, 4]
+print!w # [1, 2, 3, 4]
 ```

-Ownership transfers occur when an object is passed to a subroutine, for example.
-If you wish to retain ownership of the object after passing it to a subroutine, you must do cloning, freezing, or borrowing.
-However, as described below, borrowing can only be used in limited situations.
+Ownership transfer occurs, for example, when an object is passed to a subroutine.
+If you want to still have ownership after giving it away, you'll need to clone, freeze, or borrow.
+However, as will be explained later, there are limited situations in which it can be borrowed.

-## Cloning
+## replication

-Duplicate an object and transfer ownership of it. This is done by applying the `.clone` method to the real argument.
-The cloned object will be exactly the same as the original object, but independent of each other and unaffected by changes.
+Duplicate an object and transfer its ownership. It does this by applying the `.clone` method to the actual arguments.
+The duplicated object is exactly the same as the original, but independent of each other and unaffected by changes.

-Cloning is equivalent to deep copying in Python, and is generally more computationally and memory expensive than freezing and borrowing, since it re-creates the same object in its entirety.
-Subroutines that require object duplication are called "argument-consuming" subroutines.
+Duplication is equivalent to Python's deep copy, and since it recreates the same object entirely, the computation and memory costs are generally higher than freezing and borrowing.
+A subroutine that needs to duplicate an object is said to be an "argument consuming" subroutine.

-```erg
-capitalize s: Str!
-    s.capitalize!()
+``` erg
+capitalize s: Str!=
+    s. capitalize!()
    s

-s1 = !" hello"
+s1 = !"hello"
 s2 = capitalize s1.clone()
-log s2, s1 # !" HELLO hello"
+log s2, s1 # !"HELLO hello"
 ```

-## Freezing
+## freeze

-Taking advantage of the fact that immutable objects can be referenced from multiple places, a variable object is converted to an immutable object.
-This is called freezing. Freezing is used to create iterators from mutable arrays.
-Since iterators cannot be created directly from mutable arrays, they are converted to immutable arrays.
-If you do not want to destroy the array, use the [`.freeze_map` method](./type/mut.md), etc.
+We take advantage of the fact that immutable objects can be referenced from multiple places and convert mutable objects to immutable objects.
+This is called freezing. Freezing is used, for example, when creating an iterator from a mutable array.
+Since you can't create an iterator directly from a mutable array, convert it to an immutable array.
+If you don't want to destroy the array, use the [`.freeze_map` method](./type/mut.md).

-```erg
-# Calculate the sum of the values produced by the iterator
+``` erg
+# Compute the sum of the values produced by the iterator
 sum|T <: Add + HasUnit| i: Iterator T = ...

-x = [1, 2, 3].into [Int; !3].
+x = [1, 2, 3].into [Int; !3]
 x.push!(4)
-i = x.iter() # TypeError: [Int; !4] has no method `iter`.
+i = x.iter() # TypeError: [Int; !4] has no method `iter`
 y = x.freeze()
 i = y.iter()
 assert sum(i) == 10
-y # y is still touched after this.
+y # y can still be touched
 ```

-## Borrowing
+## borrow

-Borrowing is less expensive than cloning or freezing.
-Borrowing can be done in simple cases such as the following.
+Borrowing is cheaper than duplicating or freezing.
+Borrowing can be done in the following simple cases:

-```erg
+``` erg
 peek_str ref(s: Str!) =
    log s

-s = !" hello"
+s = !"hello"
 peek_str s
 ```

-The borrowed value is called a __reference__ to the original object.
-You can "subloan" a reference to another subroutine, but you can't consume it because you are only borrowing it.
+A borrowed value is called a __reference__ to the original object.
+You can "sublease" the reference to another subroutine, but you cannot consume it because you are only borrowing it.

-```erg
-steal_str ref(s: Str!) =.
-    # The log function only borrows arguments, so it can subloan
+``` erg
+steal_str ref(s: Str!) =
+    # Since the log function only borrows the arguments, it can be sub-leased
    log s
-    # Discard function consumes arguments, so it is an error
+    # error because the discard function consumes arguments
    discard s # OwnershipError: cannot consume a borrowed value
    # hint: use `clone` method
 ```

-```erg
+``` erg
 steal_str ref(s: Str!) =
-    # this is also no good (= consumes the right side)
+    # This is no good either (= consumes the right side)
    x = s # OwnershipError: cannot consume a borrowed value
    x
 ```

-Erg references are more restrictive than Rust. Although references are first-class objects in the language, they cannot be created explicitly and can only be specified as a way of passing real arguments by `ref`/`ref!`.
-This means that it is not possible to pack references into arrays or create classes with references as attributes.
+Erg's references are more restrictive than Rust's. References are first-class objects in the language, but cannot be created explicitly, they can only be specified as argument passing via `ref`/`ref!`.
+This means that you cannot stuff references into arrays or create classes with references as attributes.

-However, such restrictions are common in languages without references, so they are not that inconvenient.
+However, such restrictions are a natural specification in languages without references in the first place, and they are not so inconvenient.

-## Circular references
+## circular references

-Erg is designed to prevent unintentional memory leaks, and the memory checker will generate an error when it detects a circular reference. In most cases, this error can be resolved with a weak reference `Weak`. However, this does not allow the creation of objects with circular structures such as cyclic graphs, so we plan to implement an API that can create circular references as an unsafe operation.
+Erg is designed to prevent unintentional memory leaks, and will issue an error if the memory checker detects a circular reference. In most cases, this error can be resolved with a weak reference `Weak`. However, since it is not possible to generate objects with circular structures such as cyclic graphs, we plan to implement an API that can generate circular references as unsafe operations.

 <p align='center'>
    <a href='./17_mutability.md'>Previous</a> | <a href='./19_visibility.md'>Next</a>
-</p>
+</p>
--- a/doc/EN/syntax/19_visibility.md
+++ b/doc/EN/syntax/19_visibility.md
@ -1,56 +1,56 @@
 # Visibility

 Erg variables have the concept of __visibility__.
-All variables we have seen so far are called __private variables__. These are variables that are invisible to the outside world.
-For example, a private variable defined in the `foo` module cannot be referenced from another module.
+All the variables we've seen so far are called __private variables__. This is an externally invisible variable.
+For example, a private variable defined in the `foo` module cannot be referenced by another module.

-```erg
+``` erg
 # foo.er
 x = "this is an invisible variable"
 ```

-```erg
-# bar.er
+``` erg
+#bar.er
 foo = import "foo"
 foo.x # AttributeError: Module 'foo' has no attribute 'x' ('x' is private)
 ```

-In contrast, there is also a __public variable__, which can be referenced externally.
+On the other hand, there are also __public variables__, which can be referenced from the outside.
 Public variables are defined with `.`.

-```erg
+``` erg
 # foo.er
 .x = "this is a visible variable"
 ```

-```erg
-# bar.er
+``` erg
+#bar.er
 foo = import "foo"
 assert foo.x == "this is a visible variable"
 ```

-Private variables do not need to be marked with anything, but can be marked with `::` or `self::` (or `Self::` for types, etc.) to make them explicitly private. A module can also be `module::`.
+You don't need to add anything to private variables, but you can also add `::` or `self::` (`Self::` for types etc.) to indicate that they are private. increase. It can also be `module::` if it is a module.

-```erg
+``` erg
 ::x = "this is an invisible variable"
 assert ::x == x
-assert self::x == ::x
+assert self ::x == ::x
 assert module::x == ::x
 ```

-In the context of mere sequential execution, private variables are almost synonymous with local variables. They can be referenced from inner scope.
+In the context of purely sequential execution, private variables are almost synonymous with local variables. It can be referenced from the inner scope.

-```erg
+``` erg
 ::x = "this is a private variable"
 y =
    x + 1 # exactly module::x
 ```

-The `::` allows you to distinguish between variables with the same name in a scope.
-Specify the scope of the variable you want to reference on the left. For the top level, specify `module`.
-If not specified, the innermost variable is referenced as in the normal case.
+By using `::`, you can distinguish variables with the same name within the scope.
+Specify the scope of the variable you want to refer to on the left. Specify `module` for the top level.
+If not specified, the innermost variable is referenced as usual.

-```erg
+``` erg
 ::x = 0
 assert x == 0
 y =
@ -64,38 +64,38 @@ y =
        assert module::x == 0
 ```

-In the scope of an anonymous subroutine, `self` specifies its own scope.
+In the anonymous subroutine scope, `self` specifies its own scope.

-```erg
+``` erg
 x = 0
 f = x ->
    log module::x, self::x
-f 1 # 0 1
+f1# 0 1
 ```

 `::` is also responsible for accessing private instance attributes.

-```erg
+``` erg
 x = 0
 C = Class {x = Int}
 C.
-    # Top-level x is referenced (warns to make it module::x)
+    # Top-level x is referenced (warning to use module::x)
    f1 self = x
-    # x of instance attribute is referenced
+    # instance attribute x is referenced
    f2 self = self::x
 ```

 ## Visibility in external modules

-A class defined in one module can actually define methods from an external module as well.
+A class defined in one module can actually define methods from an external module.

-```erg
-## foo.er
+``` erg
+# foo.er
 .Foo = Class()
 ```

-```erg
-# bar.er
+``` erg
+#bar.er
 {Foo; ...} = import "foo"

 Foo::
@ -109,45 +109,45 @@ Foo.
    foo::private() # AttributeError
 ```

-However, both of those methods can only be used within that module.
-Externally defined private methods can be referenced by methods of the `Foo` class only within the defining module.
-Public methods are exposed outside the class, but not to outside the module.
+However, both of those methods are only available within that module.
+Private methods defined externally are visible to methods of the `Foo` class only within the defining module.
+Public methods are exposed outside the class, but not outside the module.

-```erg
-# baz.er.
+``` erg
+# baz.er
 {Foo; ...} = import "foo"

 foo = Foo.new()
 foo.public() # AttributeError: 'Foo' has no attribute 'public' ('public' is defined in module 'bar')
 ```

-Also, you cannot define a method on the type you are re-exporting.
-This is to avoid confusion when a method is found or not found depending on the module from which it is imported.
+Also, methods cannot be defined in the type to be re-exported.
+This is to avoid confusion about methods being found or not found depending on the module they are imported from.

-```erg
-# bar.er
+``` erg
+#bar.er
 {.Foo; ...} = import "foo"

 .Foo::
    private self = pass # Error
-.Foo.
-    Foo:: public self = self::private() # Error
+Foo.
+    public self = self::private() # Error
 ```

 If you want to do something like this, define a [patch](./type/07_patch.md).

-```erg
-# bar.er.
+``` erg
+#bar.er
 {Foo; ...} = import "foo"

 FooImpl = Patch Foo
-FooImpl::
+FooImpl :=:
    private self = pass
-FooImpl.
+Foo Impl.
    public self = self::private()
 ```

-```erg
+``` erg
 # baz.er
 {Foo; ...} = import "foo"
 {FooImpl; ...} = import "bar"
@ -156,7 +156,7 @@ foo = Foo.new()
 foo.public()
 ```

-## Restricted Public Variables
+## restricted public variables

 Variable visibility is not limited to complete public/private.
 You can also publish with restrictions.
@ -164,14 +164,14 @@ You can also publish with restrictions.
 ``` erg
 # foo.er
 .record = {
-     .a = {
-         .(.record)x = 0
-         .(module)y = 0
-         .z = 0
-     }
-     _ = .a.x # OK
-     _ = .a.y # OK
-     _ = .a.z # OK
+    .a = {
+        .(.record)x = 0
+        .(module)y = 0
+        .z = 0
+    }
+    _ = .a.x # OK
+    _ = .a.y # OK
+    _ = .a.z # OK
 }

 _ = .record.a.x # VisibilityError
@ -187,5 +187,5 @@ _ = foo.record.a.z # OK
 ```

 <p align='center'>
-     <a href='./18_ownership.md'>Previous</a> | <a href='./20_naming_rule.md'>Next</a>
-</p>
+    <a href='./18_ownership.md'>Previous</a> | <a href='./20_naming_rule.md'>Next</a>
+</p>
--- a/doc/EN/syntax/20_naming_rule.md
+++ b/doc/EN/syntax/20_naming_rule.md
@ -1,38 +1,38 @@
-# Naming Conventions
+# Naming convention

-If a variable is to be used as a constant expression, it must begin with a capital letter. The second and succeeding letters may be in lowercase.
+If you want to use a variable as a constant expression, make sure it starts with a capital letter. Two or more letters may be lowercase.

-```erg
+``` erg
 i: Option Type = Int
 match i:
    t: Type -> log "type"
    None -> log "None"
 ```

-Objects with side-effects must end with `!` must end with `!`. They are procedures, procedural methods, and mutable types.
-However, the `Proc` type itself is not a mutable type.
+Objects with side effects always end with `!`. Procedures and procedural methods, and mutable types.
+However, the `Proc` type itself is not mutable.

-```erg
+``` erg
 # Callable == Func or Proc
 c: Callable = print!
 match c:
-    p! -> log "proc" # can omit `: Proc` since it is self-explanatory
+    p! -> log "proc" # `: Proc` can be omitted since it is self-explanatory
    f -> log "func"
 ```

-If you want to expose the attribute to the outside world, define it with `.`. `.` attribute is not prefixed, the attribute is not public. To avoid confusion, they cannot coexist in the same scope.
+If you want to expose an attribute to the outside world, define it with `.` at the beginning. If you don't put `.` at the beginning, it will be private. To avoid confusion, they cannot coexist within the same scope.

-```erg
+``` erg
 o = {x = 1; .x = 2} # SyntaxError: private and public variables with the same name cannot coexist
 ```

 ## Literal Identifiers

-The above rule can be avoided by enclosing the string in single quotes (''). That is, a procedural object can also be assigned without `!`. In this case, however, even if the value is a constant expression, it is not considered a constant.
-Such a string identifier enclosed in single quotes is called a literal identifier.
-This is used when calling the API (FFI) of other languages such as Python.
+The above rule can be circumvented by enclosing the string in single quotes (''). That is, procedural objects can also be assigned without `!`. However, in this case, even if the value is a constant expression, it is not considered a constant.
+A character string enclosed in single quotes like this is called a literal identifier.
+This is used when calling APIs (FFI) of other languages such as Python.

-```erg
+``` erg
 bar! = pyimport("foo").'bar'
 ```

@ -40,11 +40,11 @@ Identifiers that are also valid in Erg do not need to be enclosed in ''.

 Furthermore, literal identifiers can contain both symbols and spaces, so strings that cannot normally be used as identifiers can be used as identifiers.

-```erg
+``` erg
 '∂/∂t' y
 'test 1: pass x to y'()
 ```

 <p align='center'>
    <a href='./19_visibility.md'>Previous</a> | <a href='./21_lambda.md'>Next</a>
-</p>
+</p>
--- a/doc/EN/syntax/21_lambda.md
+++ b/doc/EN/syntax/21_lambda.md
@ -1,94 +1,95 @@
-# Anonymous Function
+# anonymous function

-An anonymous function is a syntax for creating function objects on the fly without naming them.
+Anonymous functions are a syntax for creating function objects on the fly without naming them.

-```erg
-# `->` is the anonymous function operator
+``` erg
+# `->` is an anonymous function operator
 # same as `f x, y = x + y`
 f = (x, y) -> x + y
 # same as `g(x, y: Int): Int = x + y`
 g = (x, y: Int): Int -> x + y
 ```

-You can omit `()` if there is only one argument.
+You can omit the `()` if there is only one argument.

-```erg
-assert [1, 2, 3].map_collect(i -> i + 1) == [2, 3, 4].
-assert ((i, j) -> [i, j])(1, 2) == [1, 2].
+``` erg
+assert [1, 2, 3].map_collect(i -> i + 1) == [2, 3, 4]
+assert ((i, j) -> [i, j])(1, 2) == [1, 2]
 ```

-In the case below `0..9, (i -> ...)`, not `(0..9, i) -> ...`.
-`->` takes only one argument on the left side. Multiple arguments are taken as a single tuple.
+In the case below it is `0..9, (i -> ...)` and not `(0..9, i) -> ...`.
+`->` takes only one argument on the left side. Multiple arguments are received as a single tuple.

-```erg
+``` erg
 for 0..9, i: Int ->
    ...
 ```

-For anonymous functions, there is a difference in syntactic interpretation due to whitespace.
+In anonymous functions, there is a difference in parsing due to whitespace.

-```erg
-# In this case, it is interpreted as ``T(() -> Int)``.
-i: T () -> Int
-# In this case, it is interpreted as (U()) -> Int
+``` erg
+# In this case, interpreted as `T(() -> Int)`
+i: T() -> Int
+# in this case it is interpreted as (U()) -> Int
 k: U() -> Int
 ```

-Anonymous functions can be used without arguments. `=>` is an anonymous procedure operator.
+Anonymous functions can be used without arguments.

-```erg
-p!= () => print!"`p!` was called"
-# `() ->`, `() =>` have the sugar-coated constructs `do`, `do!`.
+``` erg
+# `=>` is an anonymous procedure operator
+p! = () => print! "`p!` was called"
+# `() ->`, `() =>` have syntax sugar `do`, `do!`
 # p! = do! print! "`p!` was called"
 p!() # `p!` was called
 ```

-Argumentless functions can be used for lazy initialization.
+No-argument functions can be used for lazy initialization.

-```erg
+``` erg
 time = import "time"
 date = import "datetime"
 now = if! True:
-    do!
-        time.sleep!
+    do!:
+        time. sleep! 1000
        date.now!()
    do date.new("1970", "1", "1", "00", "00")
 ```

-Typing and pattern matching can also be done. For this reason, the ``match`` function is realized almost entirely by the power of anonymous functions.
-The anonymous functions given as arguments to the ``match`` function are tried in order from the top. So, it is necessary to describe special cases at the top and more general cases as you go down. If you get the order wrong (as far as possible), the compiler will issue a Warning.
+You can also type and pattern match. Because of this, the `match` function is mostly implemented with the power of anonymous functions.
+Anonymous functions given as arguments to the `match` function are tried in order from the top. So, you should describe the special cases at the top and the more general cases at the bottom. If you get the order wrong, the compiler will issue a warning (if possible).

-```erg
-n = (Complex or Ratio or Int).sample!
-i = match n:
+``` erg
+n = (Complex or Ratio or Int).sample!()
+i = matchn:
    PI -> PI # if equal to constant PI
-    (i: 1..10) -> i # if 1~10 Int
-    (i: Int) -> i # for Int
-    (c: Complex) -> c.real() # case of Complex, Int < Complex, but can fall back
-    _ -> panic "cannot convert to Int" # none of the above; match must cover all patterns
+    For (i: 1..10) -> i # Int from 1 to 10
+    (i: Int) -> i # Int
+    (c: Complex) -> c.real() # For Complex. Int < Complex, but can fallback
+    _ -> panic "cannot convert to Int" # If none of the above apply. match must cover all patterns
 ```

-Error handling can also be done using `?` or `match`.
+Error handling is also generally done using `?` or `match`.

-```erg
+``` erg
 res: ParseResult Int
-match res:
+matchres:
    i: Int -> i
    err: Error -> panic err.msg

 res2: Result Int, Error
 match res2:
-    ok: Not Error -> log Typeof ok
+    ok: Not Error -> log Type of ok
    err: Error -> panic err.msg
 ```

-## Anonymous Polymorphic Function
+## Anonymous polycorrelation coefficient

-```erg
+``` erg
 # same as id|T| x: T = x
 id = |T| x: T -> x
 ```

 <p align='center'>
    <a href='./20_naming_rule.md'>Previous</a> | <a href='./22_subroutine.md'>Next</a>
-</p>
+</p>
--- a/doc/EN/syntax/23_closure.md
+++ b/doc/EN/syntax/23_closure.md
@ -1,32 +1,32 @@
 # Closure

-Erg subroutines have a "closure" feature that captures external variables.
+Erg subroutines have a feature called a "closure" that captures external variables.

-```erg
+``` erg
 outer = 1
 f x = outer + x
 assert f(1) == 2
 ```

-Like immutable objects, mutable objects can also be captured.
+As with immutable objects, mutable objects can also be captured.

-```erg
+``` erg
 sum = !0
 for! 1..10, i =>
-    sum.add!
+    sum.add!i
 assert sum == 45

-p! x =
-    sum.add!
+p!x=
+    sum.add!x
 p!(1)
 assert sum == 46
 ```

 Note, however, that functions cannot capture mutable objects.
-If mutable objects could be referenced in a function, the following code could be written.
+If a mutable object can be referenced in a function, you can write code like the following.

-```erg
-# !!! This code is actually an error !!!
+``` erg
+# !!! This code actually gives an error !!!
 i = !0
 f x = i + x
 assert f 1 == 1
@ -34,31 +34,31 @@ i.add! 1
 assert f 1 == 2
 ```

-The function should return the same value for the same argument, but that assumption has been violated.
-Note that ``i`` is evaluated for the first time at call time.
+The function should return the same value for the same arguments, but the assumption is broken.
+Note that `i` is evaluated only at call time.

-If you want the contents of a mutable object at the time of the function definition, `.clone` it.
+Call `.clone` if you want the contents of the mutable object at the time the function was defined.

-```erg
+``` erg
 i = !0
 immut_i = i.clone().freeze()
-f x = immut_i + x
+fx = immut_i + x
 assert f 1 == 1
 i.add! 1
 assert f 1 == 1
 ```

-## Avoiding Mutable States, Functional Programming
+## avoid mutable state, functional programming

-```erg
-## Erg
+``` erg
+# Erg
 sum = !0
 for! 1..10, i =>
-    sum.add!
+    sum.add!i
 assert sum == 45
 ```

-The equivalent program above can be written in Python as follows.
+The equivalent program above can be written in Python as follows:

 ```python
 # Python
@ -68,29 +68,29 @@ for i in range(1, 10):
 assert sum == 45
 ```

-However, Erg recommends a simpler way of writing.
-Instead of using subroutines and mutable objects to carry around state, the style is to localize the state using functions. This is called functional programming.
+However, Erg recommends a simpler notation.
+Instead of carrying around state using subroutines and mutable objects, use a style of localizing state using functions. This is called functional programming.

-```erg
+``` erg
 # Functional style
 sum = (1..10).sum()
 assert sum == 45
 ```

-The above code produces exactly the same result as the previous one, but it can be seen that this one is much simpler.
+The code above gives exactly the same result as before, but you can see that this one is much simpler.

-The `fold` function can be used to perform a variety of operations other than summing.
+The `fold` function can be used to do more than sum.
 `fold` is an iterator method that executes the argument `f` for each iteration.
-The initial value of the counter to accumulate the results is specified by `init` and accumulated in `acc`.
+The initial value of the counter that accumulates results is specified in `init` and accumulated in `acc`.

-```erg
+``` erg
 # start with 0, result will
 sum = (1..10).fold(init: 0, f: (acc, i) -> acc + i)
 assert sum == 45
 ```

-Erg is designed to be a natural and concise description of programming with invariant objects.
+Erg is designed to be a natural succinct description of programming with immutable objects.

 <p align='center'>
    <a href='./22_subroutine.md'>Previous</a> | <a href='./24_module.md'>Next</a>
-</p>
+</p>
--- a/doc/EN/syntax/24_module.md
+++ b/doc/EN/syntax/24_module.md
@ -39,4 +39,4 @@ Since module types are also record types, deconstruction assignment is possible.

 <p align='center'>
     <a href='./23_closure.md'>Previous</a> | <a href='./25_object_system.md'>Next</a>
-</p>
+</p>
--- a/doc/EN/syntax/25_object_system.md
+++ b/doc/EN/syntax/25_object_system.md
@ -1,64 +1,68 @@
 # Object

-All data that can be assigned to a variable. The `Object` class has the following attributes.
+All data that can be assigned to a variable. The attributes of the `Object` class are as follows.

-* `. __repr__`: returns a (non-rich) string representation of the object.
-* `. __sizeof__`: returns the size of the object (including heap allocation).
-* `. __dir__`: return a list of attributes of the object.
-* `. __hash__`: return the hash value of the object.
-* `. __getattribute__`: retrieve and return an object's attributes * `.
-* `.clone`: create and return a clone of an object (an independent entity in memory).
-* `.copy`: return a copy of an object (identical in memory).
+* `.__repr__`: Returns a (non-rich) string representation of the object
+* `.__sizeof__`: Returns the size of the object (including heap allocation)
+* `.__dir__`: Returns a list of object attributes
+* `.__hash__`: returns the hash value of the object
+* `.__getattribute__`: Get and return an attribute of an object
+* `.clone`: Creates and returns a clone of an object (with an independent entity in memory)
+* `.copy`: Returns a copy of the object (pointing to the same thing in memory)

 ## Record

-An object created by a record literal (`{attr = value; ...}`).
-This object can be a `.clone` or a `. __sizeof__` and other basic methods.
+An object generated by a record literal (`{attr = value; ...}`).
+This object has basic methods such as `.clone` and `.__sizeof__`.

-```erg
+``` erg
 obj = {.x = 1}
 assert obj.x == 1

-obj2 = {. .x; .y = 2}
+obj2 = {...x; .y = 2}
 assert obj2.x == 1 and obj2.y == 2
 ```

 ## Attribute

-An object associated with an object. In particular, a subroutine attribute that takes itself (`self`) as its implicit first argument is called a method.
+An object associated with an object. In particular, a subroutine attribute that takes self (`self`) as its implicit first argument is called a method.

-```erg
-# Note that private_attr does not have `. Note that there is no `.
+``` erg
+# note that there is no `.` in private_attr
 record = {.public_attr = j; private_attr = 2; .method = self -> self.i + 1}
-record.public_attr == 2
+record. public_attr == 2
 record.private_attr # AttributeError: private_attr is private
 assert record.method() == 3
 ```

 ## Element

-An object belonging to a specific type (e.g. `1` is an element of type `Int`). All objects are at least `{=}` type.
-In the case of an element of a class, it is sometimes called an instance.
+An object belonging to a particular type (e.g. `1` is an element of type `Int`). All objects are at least elements of type `{=}`.
+Elements of classes are sometimes called instances.

 ## Subroutine

-An object that is an instance of a function or procedure (including methods). The class representing a subroutine is `Subroutine`.
-More generally, `.__call__` is called a `Callable`.
+Indicates an object that is an instance of a function or procedure (including methods). The class representing a subroutine is `Subroutine`.
+An object that implements `.__call__` is more commonly called a `Callable`.

 ## Callable

-Object that implements `.__call__`. Superclass of `Subroutine`.
+An object that implements `.__call__`. It is also the superclass of `Subroutine`.

 ## Type

-An object that defines required attributes and makes objects common.
-There are two main types: polymorphic type and monomorphic type. Typical monomorphic types are `Int`, `Str`, etc. Polymorphic types include `Option Int`, `[Int; 3]` and so on.
-In addition, types that define methods to change the state of an object are called mutable types, and require variable attributes marked with `!` (e.g., dynamic arrays: `[T; !_]`).
+An object that defines requirement attributes and commonizes objects.
+There are two main types: Polymorphic Type and Monomorphic Type. Typical monomorphic types are `Int`, `Str`, etc., and polymorphic types are `Option Int`, `[Int; 3]`, etc.
+Furthermore, a type that defines a method that changes the state of an object is called a Mutable type, and it is necessary to add `!` to the variable attribute (e.g. dynamic array: `[T; !_]`) .
+
+## Class
+
+A type that has `.__new__`, `.__init__` methods, etc. Implement class-based object orientation.

 ## Function

-Subroutines that have read permission for external variables (excluding static variables) but do not have read/write permission for external variables. In other words, it has no external side effects.
-Erg functions are defined differently than Python because they do not allow side effects.
+A subroutine that has read permission for external variables (excluding static variables) but does not have read/write permission for external variables. In other words, it has no external side effects.
+Erg functions are defined differently than Python's because they do not allow side effects.

 ## Procedure

@ -71,8 +75,8 @@ A subroutine that implicitly takes `self` as the first argument. It is a differe
 ## Entity

 Objects that are not subroutines and types.
-Monomorphic entities (`1`, `"a"`, etc.) are also called value objects, and polymorphic entities (`[1, 2, 3], {"a": 1}`) are also called container objects.
+Monomorphic entities (`1`, `"a"`, etc.) are also called value objects, polymorphic entities (`[1, 2, 3], {"a": 1}`) are also called container objects .

 <p align='center'>
    <a href='./24_module.md'>Previous</a> | <a href='./26_pattern_matching.md'>Next</a>
-</p>
+</p>
--- a/doc/EN/syntax/26_pattern_matching.md
+++ b/doc/EN/syntax/26_pattern_matching.md
@ -1,52 +1,56 @@
-# Pattern matching, Irrefutability
+# pattern matching, refutable

-## Patterns Available in Erg
+## Patterns available in Erg

-### Variable Pattern
+### variable pattern

-```erg
-# basic assignment
+``` erg
+# basic assignments
 i = 1
 # with type
 i: Int = 1
 # with anonymous type
 i: {1, 2, 3} = 2
-# function
+
+# functions
 fn x = x + 1
 # equals
 fn x: Add(Int) = x + 1
 # (anonymous) function
 fn = x -> x + 1
 fn: Int -> Int = x -> x + 1
+
 # higher-order type
 a: [Int; 4] = [0, 1, 2, 3]
 # or
-a: Array Int, 4 = [0, 1, 2, 3] # or
+a: Array Int, 4 = [0, 1, 2, 3]
 ```

-### Literal Pattern
+### Literal patterns

-```erg
-# if `i` cannot be determined to be 1 at compile time, TypeError occurs.
-# short hand of `_: {1} = i`
+``` erg
+# Raise a TypeError if `i` cannot be determined to be 1 at compile time.
+# omit `_: {1} = i`
 1 = i
+
 # simple pattern matching
 match x:
    1 -> "1"
    2 -> "2"
    _ -> "other"
+
 # fibonacci function
-fib 0 = 0
-fib 1 = 1
-fib n: Nat = fib n-1 + fib n-2
+fib0 = 0
+fib1 = 1
+fibn: Nat = fibn-1 + fibn-2
 ```

-### Constant Pattern
+### constant pattern

-```erg
-cond = False
+``` erg
+cond=False
 match! cond:
-    True => print!
+    True => print! "cond is True"
    _ => print! "cond is False"

 PI = 3.141592653589793
@ -58,61 +62,61 @@ name = match num:
    _ -> "unnamed"
 ```

-### Refinement Pattern
+### Sieve pattern

-```erg
+``` erg
+# these two are the same
 Array(T, N: {N | N >= 3})
-# == ==
 Array(T, N | N >= 3)

 f M, N | M >= 0, N >= 1 = ...
 f(1, 0) # TypeError: N (2nd parameter) must be 1 or more
 ```

-### Discard (Wildcard) Pattern
+### discard (wildcard) pattern

-```erg
+``` erg
 _ = 1
 _: Int = 1
-zero _ = 0
+zero_ = 0
 right(_, r) = r
 ```

-### Varargs Patterns
+### Variable length patterns

-Used in combination with the tuple/array/record pattern described below.
+It is used in combination with the tuple/array/record pattern described later.

-```erg
-[i, . .j] = [1, 2, 3, 4]
-assert j == [2, 3, 4].
+``` erg
+[i,...j] = [1, 2, 3, 4]
+assert j == [2, 3, 4]
 first|T|(fst: T, ...rest: T) = fst
 assert first(1, 2, 3) == 1
 ```

-### Tuple Pattern
+### Tuple pattern

-```erg
+``` erg
 (i, j) = (1, 2)
 ((k, l), _) = ((1, 2), (3, 4))
-# () can be omitted if not nested (1, 2 are treated as (1, 2))
+# If not nested, () can be omitted (1, 2 are treated as (1, 2))
 m, n = 1, 2

 f(x, y) = ...
 ```

-### Array Pattern
+### array pattern

-```erg
+``` erg
 [i, j] = [1, 2]
 [[k, l], _] = [[1, 2], [3, 4]]

-length [] = 0
-length [_, . .rest] = 1 + length rest
+length[] = 0
+length[_, ...rest] = 1 + lengthrest
 ```

-### Record Pattern
+#### record pattern

-```erg
+``` erg
 record = {i = 1; j = 2; k = 3}
 {j; ...} = record # i, k will be freed

@ -127,9 +131,9 @@ age = match person:
 f {x: Int; y: Int} = ...
 ```

-### Data Class Pattern
+### Data class pattern

-```erg
+``` erg
 Point = Inherit {x = Int; y = Int}
 p = Point::{x = 1; y = 2}
 Point::{x; y} = p
@ -144,46 +148,46 @@ List T.
            _ -> ...
    second self =
        match self:
-            Cons::{rest=Cons::{head; ...} ; ...} -> head
+            Cons::{rest=Cons::{head; ...}; ...} -> head
            _ -> ...
 ```

-### Enumeration Pattern
+### enumeration pattern

-* actually just an enumerated type
+*Actually, it's just an enumeration type

-```erg
+``` erg
 match x:
    i: {1, 2} -> "one or two: {i}"
    _ -> "other"
 ```

-### Range Pattern
+### range pattern

-* actually just an interval type
+*Actually, it is just an interval type.

-```erg
+``` erg
 # 0 < i < 1
-i: 0<... <1 = 0.5
+i: 0<..<1 = 0.5
 # 1 < j <= 2
-_: {[I, J] | I, J: 1<. .2} = [1, 2]
+_: {[I, J] | I, J: 1<..2} = [1, 2]
 # 1 <= i <= 5
 match i
    i: 1..5 -> ...
 ```

-### Non-patterns and Non-patternable Items
+### Things that aren't patterns, things that can't be patterned

-A pattern is something that can be uniquely specified. In this respect, pattern matching differs from ordinary conditional branching.
+A pattern is something that can be uniquely specified. In this respect pattern matching differs from ordinary conditional branching.

-The specification of a condition is not unique. For example, to determine whether the number `n` is even, the orthodox way is `n % 2 == 0`, but it can also be written as `(n / 2).round() == n / 2`.
-The non-unique form is non-trivial, whether it works correctly or is equivalent to another condition.
+Condition specifications are not unique. For example, to check if the number `n` is even, the orthodox is `n % 2 == 0`, but you can also write `(n / 2).round() == n / 2`.
+A non-unique form is not trivial whether it works correctly or is equivalent to another condition.

-#### Set
+#### set

-There is no pattern for sets. There is no pattern for sets because there is no way to retrieve elements uniquely.
-They can be retrieved with an iterator, but the order is not guaranteed.
+There is no set pattern. Because the set has no way to uniquely retrieve the elements.
+You can retrieve them by iterator, but the order is not guaranteed.

 <p align='center'>
    <a href='./25_object_system.md'>Previous</a> | <a href='./27_comprehension.md'>Next</a>
-</p>
+</p>
--- a/doc/EN/syntax/27_comprehension.md
+++ b/doc/EN/syntax/27_comprehension.md
@ -1,56 +1,65 @@
 # Comprehension

-An array can be created by `[expr | (name <- iterable)+ (predicate)*]`,
-And a set can be created by `{expr | (name <- iterable)+ (predicate)*}`.
+Array with `[expr | (name <- iterable)+ (predicate)*]`,
+set with `{expr | (name <- iterable)+ (predicate)*}`,
+You can create a Dict with `{key: value | (name <- iterable)+ (predicate)*}`.

-Dict can be created by `{key: value | (name <- iterable)+ (predicate)*}`.
+The first part of the clauses separated by `|` is called the layout clause (location clause), the second part is called the bind clause (binding clause), and the third part is called the guard clause (conditional clause).
+A guard clause can be omitted, but a bind clause cannot be omitted, and a guard clause cannot precede a bind clause.

-The first part of a clause delimited by `|` is called a layout clause, the second part is called a bind clause, and the third part is called a guard clause.
-The guard clause can be omitted, but not the bind clause, and the guard clause cannot be placed before the bind clause.
+Comprehension example

-e.g.
+``` erg
+# the layout clause is i
+# bind clause is i <- [0, 1, 2]
+assert [i | i <- [0, 1, 2]] == [0, 1, 2]

-```erg
-assert [i | i <- [0, 1, 2]] == [0, 1, 2]]
-assert [i / 2 | i <- 0..2] == [0.0, 0.5, 1.0]]
+# layout clause is i / 2
+# bind clause is i <- 0..2
+assert [i/2 | i <- 0..2] == [0.0, 0.5, 1.0]
+
+# layout clause is (i, j)
+# bind clause i <- 0..2, j <- 0..2
+# guard clause is (i + j) % 2 == 0
 assert [(i, j) | i <- 0..2; j <- 0..2; (i + j) % 2 == 0] == [(0, 0), (0, 2), (1, 1), (2, 0), (2, 2)]
+
 assert {i % 2 | i <- 0..9} == {0, 1}
 assert {k: v | k <- ["a", "b"]; v <- [1, 2]} == {"a": 1, "b": 2}
 ```

-Erg's comprehension notation is influenced by Haskell, but there are some differences.
-In Haskell's list comprehensions, the order of variables makes a difference in the result, but not in Erg.
+Erg comprehensions are inspired by Haskell, but with some differences.
+For Haskell list comprehensions, the order of variables makes a difference in the result, but in Erg it doesn't matter.

-```haskell
+``` haskell
 -- Haskell
-[(i, j) | i <- [1..3], j <- [3..5]] == [(1,3),(1,4),(1,5),(2,3),(2,4),(2,5),(3,3),(3,4),(3,5)]
-[(i, j) | j <- [3..5], i <- [1..3]] == [(1,3),(2,3),(3,3),(1,4),(2,4),(3,4),(1,5),(2,5),(3,5)]
+[(i, j) | i <- [1..3], j <- [3..5]] == [(1,3),(1,4),(1,5),(2 ,3),(2,4),(2,5),(3,3),(3,4),(3,5)]
+[(i, j) | j <- [3..5], i <- [1..3]] == [(1,3),(2,3),(3,3),(1 ,4),(2,4),(3,4),(1,5),(2,5),(3,5)]
 ```

-```erg
+``` erg
 # Erg
-assert [(i, j) | i <- 1. <3; j <- 3.. <5] == [(i, j) | j <- 3.. <5; i <- 1.. <3]
+assert [(i, j) | i <- 1..<3; j <- 3..<5] == [(i, j) | j <- 3..<5; i <- 1.. <3]
 ```

-これはPythonと同じである。
+This specification is the same as that of Python.

 ```python
 # Python
 assert [(i, j) for i in range(1, 3) for j in range(3, 5)] == [(i, j) for j in range(3, 5) for i in range(1, 3)]
 ```

-## Refinement type
+## Sieve type

-Similar to comprehensions are refinement types. A refinement type is a type (enumerated type) in the form `{Name: Type | Predicate}`.
-In the case of a refinement type, Name is limited to one and the layout cannot be specified (but multiple values can be handled by using a tuple type, for example), and Predicate must be a compile-time computation, i.e., a constant expression.
+Similar to comprehensions are sieve types. A sieve type is a type (enumerated type) created in the form `{Name: Type | Predicate}`.
+In the case of the sieve type, only one Name can be specified and the layout cannot be specified (however, multiple values can be handled if it is a tuple type), and the Predicate can be calculated at compile time, that is, only a constant expression can be specified.

-```erg
+``` erg
 Nat = {I: Int | I >= 0}
-# If the predicate expression is and only, it can be replaced by ;.
+# If the predicate expression is only and, it can be replaced with ;
 # Nat2D = {(I, J): (Int, Int) | I >= 0; J >= 0}
 Nat2D = {(I, J): (Int, Int) | I >= 0 and J >= 0}
 ```

 <p align='center'>
    <a href='./26_pattern_matching.md'>Previous</a> | <a href='./28_spread_syntax.md'>Next</a>
-</p>
+</p>
--- a/doc/EN/syntax/28_spread_syntax.md
+++ b/doc/EN/syntax/28_spread_syntax.md
@ -1,42 +1,42 @@
 # Spread assignment

-In a spread assignment, a variable can be prefixed with `...` in front of the variable, all the remaining elements can be expanded into the variable. This is called a spread assignment.
+In a decomposing assignment, putting `...` in front of a variable expands all remaining elements into that variable. This is called expansion assignment.

-```erg
-[x, ... .y] = [1, 2, 3]
+``` erg
+[x,...y] = [1, 2, 3]
 assert x == 1
-assert y == [2, 3].
-x, ... .y = (1, 2, 3)
+assert y == [2, 3]
+x, ...y = (1, 2, 3)
 assert x == 1
 assert y == (2, 3)
 ```

 ## Extract assignment

-If nothing is written after `...`, the remaining elements are ignored and an assignment is made. This type of expansion assignment is specifically called an extract assignment.
-Extract assignment is a useful syntax for bringing certain attributes local to a module or record.
+If nothing is written after `...`, the remaining elements are ignored and assigned. This type of expansion assignment is specifically called extractive assignment.
+Extraction assignment is a convenient syntax for localizing specific attributes within a module or record.

-```erg
-{sin; cos; tan; ...} = import "math"
+``` erg
+{sin; cos; tan; ..} = import "math"
 ```

-This way, `sin`, `cos`, `tan` can be used locally from then on.
+After that, you can use `sin, cos, tan` locally.

 You can do the same with records.

-```erg
+``` erg
 record = {x = 1; y = 2}
 {x; y; ...} = record
 ```

-If you want to expand all of them, use `{*} = record`, this is equivalent to `open` in OCaml and so on.
+If you want to expand all, use `{*} = record`. It is `open` in OCaml.

-```erg
+``` erg
 record = {x = 1; y = 2}
-{*} = record
+{*} = records
 assert x == 1 and y == 2
 ```

 <p align='center'>
    <a href='./27_comprehension.md'>Previous</a> | <a href='./29_decorator.md'>Next</a>
-</p>
+</p>
--- a/Show more
+++ b/Show more