diff --git a/compiler/erg_common/dict.rs b/compiler/erg_common/dict.rs
index 233da03f..dae08406 100644
--- a/compiler/erg_common/dict.rs
+++ b/compiler/erg_common/dict.rs
@@ -127,6 +127,14 @@ impl<K, V> Dict<K, V> {
     pub fn clear(&mut self) {
         self.dict.clear();
     }
+
+    /// remove all elements for which the predicate returns false
+    pub fn retain<F>(&mut self, f: F)
+    where
+        F: FnMut(&K, &mut V) -> bool,
+    {
+        self.dict.retain(f);
+    }
 }
 
 impl<K, V> IntoIterator for Dict<K, V> {
diff --git a/compiler/erg_compiler/codegen.rs b/compiler/erg_compiler/codegen.rs
index 82dd9e4e..ef05b483 100644
--- a/compiler/erg_compiler/codegen.rs
+++ b/compiler/erg_compiler/codegen.rs
@@ -138,6 +138,7 @@ pub struct PyCodeGenerator {
     pub(crate) py_version: PythonVersion,
     str_cache: CacheSet<str>,
     prelude_loaded: bool,
+    mutate_op_loaded: bool,
     in_op_loaded: bool,
     record_type_loaded: bool,
     module_type_loaded: bool,
@@ -154,6 +155,7 @@ impl PyCodeGenerator {
             cfg,
             str_cache: CacheSet::new(),
             prelude_loaded: false,
+            mutate_op_loaded: false,
             in_op_loaded: false,
             record_type_loaded: false,
             module_type_loaded: false,
@@ -431,7 +433,8 @@ impl PyCodeGenerator {
     }
 
     fn emit_load_const<C: Into<ValueObj>>(&mut self, cons: C) {
-        let value = cons.into();
+        let value: ValueObj = cons.into();
+        let is_int = value.is_int();
         let is_nat = value.is_nat();
         let is_bool = value.is_bool();
         if !self.cfg.no_std {
@@ -441,6 +444,9 @@ impl PyCodeGenerator {
             } else if is_nat {
                 self.emit_push_null();
                 self.emit_load_name_instr(Identifier::public("Nat"));
+            } else if is_int {
+                self.emit_push_null();
+                self.emit_load_name_instr(Identifier::public("Int"));
             }
         }
         let idx = self
@@ -455,7 +461,8 @@ impl PyCodeGenerator {
         self.write_instr(LOAD_CONST);
         self.write_arg(idx);
         self.stack_inc();
-        if !self.cfg.no_std && is_nat {
+        if !self.cfg.no_std && is_int {
+            // is_int => is_nat and is_bool
             self.emit_call_instr(1, Name);
             self.stack_dec();
         }
@@ -1290,12 +1297,18 @@ impl PyCodeGenerator {
     fn emit_unaryop(&mut self, unary: UnaryOp) {
         log!(info "entered {} ({unary})", fn_name!());
         let tycode = TypeCode::from(unary.lhs_t());
-        self.emit_expr(*unary.expr);
         let instr = match &unary.op.kind {
             // TODO:
             TokenKind::PrePlus => UNARY_POSITIVE,
             TokenKind::PreMinus => UNARY_NEGATIVE,
-            TokenKind::Mutate => NOP, // ERG_MUTATE,
+            TokenKind::Mutate => {
+                if !self.mutate_op_loaded {
+                    self.load_mutate_op();
+                }
+                self.emit_push_null();
+                self.emit_load_name_instr(Identifier::private("#mutate_operator"));
+                NOP // ERG_MUTATE,
+            }
             _ => {
                 CompileError::feature_error(
                     self.cfg.input.clone(),
@@ -1307,8 +1320,14 @@ impl PyCodeGenerator {
                 NOT_IMPLEMENTED
             }
         };
-        self.write_instr(instr);
-        self.write_arg(tycode as usize);
+        self.emit_expr(*unary.expr);
+        if instr != NOP {
+            self.write_instr(instr);
+            self.write_arg(tycode as usize);
+        } else {
+            self.emit_precall_and_call(1);
+            self.stack_dec();
+        }
     }
 
     fn emit_binop(&mut self, bin: BinOp) {
@@ -1767,7 +1786,7 @@ impl PyCodeGenerator {
     }
 
     fn emit_match_guard(&mut self, t_spec: TypeSpec, pop_jump_points: &mut Vec<usize>) {
-        #[allow(clippy::single_match)]
+        log!(info "entered {} ({t_spec})", fn_name!());
         match t_spec {
             TypeSpec::Enum(enum_t) => {
                 let elems = ValueObj::vec_from_const_args(enum_t);
@@ -1817,14 +1836,42 @@ impl PyCodeGenerator {
                 self.write_arg(0);
                 self.stack_dec();
             }
+            // _: (Int, Str)
+            TypeSpec::Tuple(tup) => {
+                let len = tup.len();
+                for (i, t_spec) in tup.into_iter().enumerate() {
+                    if i != 0 && i != len - 1 {
+                        self.dup_top();
+                    }
+                    self.emit_load_const(i);
+                    self.write_instr(Opcode311::BINARY_SUBSCR);
+                    self.write_arg(0);
+                    self.stack_dec();
+                    self.emit_match_guard(t_spec, pop_jump_points);
+                }
+            }
+            // TODO: consider ordering (e.g. both [1, 2] and [2, 1] is type of [{1, 2}; 2])
+            TypeSpec::Array(arr) => {
+                let ValueObj::Nat(len) = ValueObj::from_const_expr(arr.len) else { todo!() };
+                for i in 0..=(len - 1) {
+                    if i != 0 && i != len - 1 {
+                        self.dup_top();
+                    }
+                    self.emit_load_const(i);
+                    self.write_instr(Opcode311::BINARY_SUBSCR);
+                    self.write_arg(0);
+                    self.stack_dec();
+                    self.emit_match_guard(*arr.ty.clone(), pop_jump_points);
+                }
+            }
             /*TypeSpec::Interval { op, lhs, rhs } => {
                 let binop = BinOp::new(op, lhs.downcast(), rhs.downcast(), VarInfo::default());
                 self.emit_binop(binop);
             }*/
             // TODO:
-            other => {
-                log!(err "{other}")
-            }
+            TypeSpec::Infer(_) => unreachable!(),
+            // TODO:
+            other => log!(err "{other}"),
         }
     }
 
@@ -2015,7 +2062,7 @@ impl PyCodeGenerator {
         } else if let Some(func_name) = debind(&method_name) {
             return self.emit_call_fake_method(obj, func_name, method_name, args);
         }
-        let is_py_api = obj.is_py_api();
+        let is_py_api = method_name.is_py_api();
         self.emit_expr(obj);
         self.emit_load_method_instr(method_name);
         self.emit_args_311(args, Method, is_py_api);
@@ -2699,10 +2746,15 @@ impl PyCodeGenerator {
     }
 
     fn load_prelude(&mut self) {
+        // NOTE: Integers need to be used in IMPORT_NAME
+        // but `Int` are called before importing it, so they need to be no_std mode
+        let no_std = self.cfg.no_std;
+        self.cfg.no_std = true;
         self.load_record_type();
         self.load_prelude_py();
         self.prelude_loaded = true;
         self.record_type_loaded = true;
+        self.cfg.no_std = no_std;
     }
 
     fn load_in_op(&mut self) {
@@ -2721,6 +2773,22 @@ impl PyCodeGenerator {
         self.in_op_loaded = true;
     }
 
+    fn load_mutate_op(&mut self) {
+        let mod_name = if self.py_version.minor >= Some(10) {
+            Identifier::public("_erg_std_prelude")
+        } else {
+            Identifier::public("_erg_std_prelude_old")
+        };
+        self.emit_global_import_items(
+            mod_name,
+            vec![(
+                Identifier::public("mutate_operator"),
+                Some(Identifier::private("#mutate_operator")),
+            )],
+        );
+        self.mutate_op_loaded = true;
+    }
+
     fn load_control(&mut self) {
         let mod_name = Identifier::public("_erg_control");
         self.emit_import_all_instr(mod_name);
diff --git a/compiler/erg_compiler/context/compare.rs b/compiler/erg_compiler/context/compare.rs
index 321aa57b..0e4488f3 100644
--- a/compiler/erg_compiler/context/compare.rs
+++ b/compiler/erg_compiler/context/compare.rs
@@ -274,7 +274,7 @@ impl Context {
         if !self.is_class(lhs) || !self.is_class(rhs) {
             return (Maybe, false);
         }
-        if let Some(ty_ctx) = self.get_nominal_type_ctx(rhs) {
+        if let Some((_, ty_ctx)) = self.get_nominal_type_ctx(rhs) {
             for rhs_sup in ty_ctx.super_classes.iter() {
                 let rhs_sup = if rhs_sup.has_qvar() {
                     let rhs = match rhs {
@@ -312,7 +312,7 @@ impl Context {
         if !self.is_trait(lhs) {
             return (Maybe, false);
         }
-        if let Some(rhs_ctx) = self.get_nominal_type_ctx(rhs) {
+        if let Some((_, rhs_ctx)) = self.get_nominal_type_ctx(rhs) {
             for rhs_sup in rhs_ctx.super_traits.iter() {
                 // Not `supertype_of` (only structures are compared)
                 match self.cheap_supertype_of(lhs, rhs_sup) {
@@ -656,7 +656,7 @@ impl Context {
             erg_common::fmt_vec(lparams),
             erg_common::fmt_vec(rparams)
         );
-        let ctx = self
+        let (_, ctx) = self
             .get_nominal_type_ctx(typ)
             .unwrap_or_else(|| panic!("{typ} is not found"));
         let variances = ctx.type_params_variance();
@@ -858,9 +858,13 @@ impl Context {
             }
             (Refinement(l), Refinement(r)) => Type::Refinement(self.union_refinement(l, r)),
             (t, Type::Never) | (Type::Never, t) => t.clone(),
-            (t, Refinement(r)) | (Refinement(r), t) => {
-                let t = self.into_refinement(t.clone());
-                Type::Refinement(self.union_refinement(&t, r))
+            // ?T or {"b"} cannot be {I: (?T or Str) | I == "b"} because ?T may be {"a"} etc.
+            // (if so, {I: ?T or Str | I == "b"} == {I: {"a"} or Str | I == "b"} == {I: Str | I == "b"})
+            (other, Refinement(refine)) | (Refinement(refine), other)
+                if !other.is_unbound_var() =>
+            {
+                let other = self.into_refinement(other.clone());
+                Type::Refinement(self.union_refinement(&other, refine))
             }
             // Array({1, 2}, 2), Array({3, 4}, 2) ==> Array({1, 2, 3, 4}, 2)
             (
diff --git a/compiler/erg_compiler/context/hint.rs b/compiler/erg_compiler/context/hint.rs
index 5f1aef6e..a3d5db94 100644
--- a/compiler/erg_compiler/context/hint.rs
+++ b/compiler/erg_compiler/context/hint.rs
@@ -21,7 +21,7 @@ enum Sequence {
 
 // TODO: these should not be in Context
 impl Context {
-    fn readable_type(typ: &Type) -> Type {
+    pub(crate) fn readable_type(typ: &Type) -> Type {
         match typ {
             Type::FreeVar(fv) if fv.constraint_is_sandwiched() => {
                 let (sub, sup) = fv.get_subsup().unwrap();
diff --git a/compiler/erg_compiler/context/initialize/mod.rs b/compiler/erg_compiler/context/initialize/mod.rs
index 8d16f3ec..e367056f 100644
--- a/compiler/erg_compiler/context/initialize/mod.rs
+++ b/compiler/erg_compiler/context/initialize/mod.rs
@@ -773,6 +773,8 @@ impl Context {
         // class("Rational"),
         // class("Integral"),
         int.register_builtin_py_impl("abs", fn0_met(Int, Nat), Immutable, Public, Some("__abs__"));
+        int.register_builtin_py_impl("succ", fn0_met(Int, Int), Immutable, Public, Some("succ"));
+        int.register_builtin_py_impl("pred", fn0_met(Int, Int), Immutable, Public, Some("pred"));
         let mut int_ord = Self::builtin_methods(Some(mono("Ord")), 2);
         int_ord.register_builtin_impl(
             "__partial_cmp__",
@@ -1345,6 +1347,9 @@ impl Context {
         let mut int_mut = Self::builtin_mono_class("Int!", 2);
         int_mut.register_superclass(Int, &int);
         int_mut.register_superclass(mono("Float!"), &float_mut);
+        let t = pr_met(mono("Int!"), vec![], None, vec![kw("i", Int)], NoneType);
+        int_mut.register_builtin_py_impl("inc!", t.clone(), Immutable, Public, Some("inc"));
+        int_mut.register_builtin_py_impl("dec!", t, Immutable, Public, Some("dec"));
         let mut int_mut_mutable = Self::builtin_methods(Some(mono("Mutable")), 2);
         int_mut_mutable.register_builtin_const("ImmutType", Public, ValueObj::builtin_t(Int));
         let f_t = kw("func", func(vec![kw("old", Int)], None, vec![], Int));
diff --git a/compiler/erg_compiler/context/inquire.rs b/compiler/erg_compiler/context/inquire.rs
index be2e6c79..a511a1c9 100644
--- a/compiler/erg_compiler/context/inquire.rs
+++ b/compiler/erg_compiler/context/inquire.rs
@@ -241,7 +241,14 @@ impl Context {
         kw_args: &[hir::KwArg],
     ) -> TyCheckResult<VarInfo> {
         if !kw_args.is_empty() {
-            todo!()
+            // TODO: this error desc is not good
+            return Err(TyCheckErrors::from(TyCheckError::default_param_error(
+                self.cfg.input.clone(),
+                line!() as usize,
+                kw_args[0].loc(),
+                self.caused_by(),
+                "match",
+            )));
         }
         for pos_arg in pos_args.iter().skip(1) {
             let t = pos_arg.expr.ref_t();
@@ -267,22 +274,22 @@ impl Context {
         for (i, pos_arg) in pos_args.iter().skip(1).enumerate() {
             let lambda = erg_common::enum_unwrap!(&pos_arg.expr, hir::Expr::Lambda);
             if !lambda.params.defaults.is_empty() {
-                todo!()
+                return Err(TyCheckErrors::from(TyCheckError::default_param_error(
+                    self.cfg.input.clone(),
+                    line!() as usize,
+                    pos_args[i + 1].loc(),
+                    self.caused_by(),
+                    "match",
+                )));
             }
-            // TODO: If the first argument of the match is a tuple?
             if lambda.params.len() != 1 {
-                return Err(TyCheckErrors::from(TyCheckError::argument_error(
+                return Err(TyCheckErrors::from(TyCheckError::param_error(
                     self.cfg.input.clone(),
                     line!() as usize,
                     pos_args[i + 1].loc(),
                     self.caused_by(),
                     1,
-                    pos_args[i + 1]
-                        .expr
-                        .signature_t()
-                        .unwrap()
-                        .typarams_len()
-                        .unwrap_or(0),
+                    lambda.params.len(),
                 )));
             }
             let mut dummy_tv_cache = TyVarCache::new(self.level, self);
@@ -565,7 +572,7 @@ impl Context {
                 self.get_attr_info_from_attributive(&fv.crack(), ident, namespace)
             }
             Type::FreeVar(fv) => {
-                let sup = fv.get_sup().unwrap();
+                let sup = fv.get_super().unwrap();
                 self.get_attr_info_from_attributive(&sup, ident, namespace)
             }
             Type::Ref(t) => self.get_attr_info_from_attributive(t, ident, namespace),
@@ -1610,7 +1617,7 @@ impl Context {
         match t {
             Type::FreeVar(fv) if fv.is_linked() => self.get_nominal_super_type_ctxs(&fv.crack()),
             Type::FreeVar(fv) => {
-                if let Some(sup) = fv.get_sup() {
+                if let Some(sup) = fv.get_super() {
                     self.get_nominal_super_type_ctxs(&sup)
                 } else {
                     self.get_nominal_super_type_ctxs(&Type)
@@ -1651,7 +1658,7 @@ impl Context {
         &'a self,
         t: &Type,
     ) -> Option<impl Iterator<Item = &'a Context>> {
-        let ctx = self.get_nominal_type_ctx(t)?;
+        let (_, ctx) = self.get_nominal_type_ctx(t)?;
         let sups = ctx
             .super_classes
             .iter()
@@ -1659,18 +1666,19 @@ impl Context {
             .map(|sup| {
                 self.get_nominal_type_ctx(sup)
                     .unwrap_or_else(|| todo!("compiler bug: {sup} not found"))
+                    .1
             });
         Some(vec![ctx].into_iter().chain(sups))
     }
 
     pub(crate) fn _get_super_traits(&self, typ: &Type) -> Option<impl Iterator<Item = Type>> {
         self.get_nominal_type_ctx(typ)
-            .map(|ctx| ctx.super_traits.clone().into_iter())
+            .map(|(_, ctx)| ctx.super_traits.clone().into_iter())
     }
 
     /// if `typ` is a refinement type, include the base type (refine.t)
     pub(crate) fn _get_super_classes(&self, typ: &Type) -> Option<impl Iterator<Item = Type>> {
-        self.get_nominal_type_ctx(typ).map(|ctx| {
+        self.get_nominal_type_ctx(typ).map(|(_, ctx)| {
             let super_classes = ctx.super_classes.clone();
             let derefined = typ.derefine();
             if typ != &derefined {
@@ -1682,7 +1690,10 @@ impl Context {
     }
 
     // TODO: Never
-    pub(crate) fn get_nominal_type_ctx<'a>(&'a self, typ: &Type) -> Option<&'a Context> {
+    pub(crate) fn get_nominal_type_ctx<'a>(
+        &'a self,
+        typ: &Type,
+    ) -> Option<(&'a Type, &'a Context)> {
         match typ {
             Type::FreeVar(fv) if fv.is_linked() => {
                 if let Some(res) = self.get_nominal_type_ctx(&fv.crack()) {
@@ -1690,7 +1701,7 @@ impl Context {
                 }
             }
             Type::FreeVar(fv) => {
-                let sup = fv.get_sup().unwrap();
+                let sup = fv.get_super().unwrap();
                 if let Some(res) = self.get_nominal_type_ctx(&sup) {
                     return Some(res);
                 }
@@ -1701,37 +1712,37 @@ impl Context {
                 }
             }
             Type::Quantified(_) => {
-                if let Some((_t, ctx)) = self
+                if let Some((t, ctx)) = self
                     .get_builtins()
                     .unwrap_or(self)
                     .rec_get_mono_type("QuantifiedFunc")
                 {
-                    return Some(ctx);
+                    return Some((t, ctx));
                 }
             }
             Type::Subr(subr) => match subr.kind {
                 SubrKind::Func => {
-                    if let Some((_, ctx)) = self
+                    if let Some((t, ctx)) = self
                         .get_builtins()
                         .unwrap_or(self)
                         .rec_get_mono_type("Func")
                     {
-                        return Some(ctx);
+                        return Some((t, ctx));
                     }
                 }
                 SubrKind::Proc => {
-                    if let Some((_, ctx)) = self
+                    if let Some((t, ctx)) = self
                         .get_builtins()
                         .unwrap_or(self)
                         .rec_get_mono_type("Proc")
                     {
-                        return Some(ctx);
+                        return Some((t, ctx));
                     }
                 }
             },
             Type::Mono(name) => {
-                if let Some((_, ctx)) = self.rec_get_mono_type(&typ.local_name()) {
-                    return Some(ctx);
+                if let Some((t, ctx)) = self.rec_get_mono_type(&typ.local_name()) {
+                    return Some((t, ctx));
                 }
                 // e.g. http.client.Response -> http.client
                 let mut namespaces = name.split_with(&[".", "::"]);
@@ -1754,14 +1765,14 @@ impl Context {
                             .and_then(|cache| cache.ref_ctx(path.as_path()))
                     })
                 {
-                    if let Some((_, ctx)) = ctx.rec_get_mono_type(type_name) {
-                        return Some(ctx);
+                    if let Some((t, ctx)) = ctx.rec_get_mono_type(type_name) {
+                        return Some((t, ctx));
                     }
                 }
             }
             Type::Poly { name, .. } => {
-                if let Some((_, ctx)) = self.rec_get_poly_type(&typ.local_name()) {
-                    return Some(ctx);
+                if let Some((t, ctx)) = self.rec_get_poly_type(&typ.local_name()) {
+                    return Some((t, ctx));
                 }
                 // NOTE: This needs to be changed if we want to be able to define classes/traits outside of the top level
                 let mut namespaces = name.split_with(&[".", "::"]);
@@ -1784,8 +1795,8 @@ impl Context {
                             .and_then(|cache| cache.ref_ctx(path.as_path()))
                     })
                 {
-                    if let Some((_, ctx)) = ctx.rec_get_poly_type(type_name) {
-                        return Some(ctx);
+                    if let Some((t, ctx)) = ctx.rec_get_poly_type(type_name) {
+                        return Some((t, ctx));
                     }
                 }
             }
@@ -1793,15 +1804,13 @@ impl Context {
                 return self
                     .get_builtins()
                     .unwrap_or(self)
-                    .rec_get_mono_type("RecordType")
-                    .map(|(_, ctx)| ctx);
+                    .rec_get_mono_type("RecordType");
             }
             Type::Record(_) => {
                 return self
                     .get_builtins()
                     .unwrap_or(self)
-                    .rec_get_mono_type("Record")
-                    .map(|(_, ctx)| ctx);
+                    .rec_get_mono_type("Record");
             }
             Type::Or(_l, _r) => {
                 if let Some(ctx) = self.get_nominal_type_ctx(&poly("Or", vec![])) {
@@ -1810,8 +1819,8 @@ impl Context {
             }
             // FIXME: `F()`などの場合、実際は引数が省略されていてもmonomorphicになる
             other if other.is_monomorphic() => {
-                if let Some((_t, ctx)) = self.rec_get_mono_type(&other.local_name()) {
-                    return Some(ctx);
+                if let Some((t, ctx)) = self.rec_get_mono_type(&other.local_name()) {
+                    return Some((t, ctx));
                 }
             }
             Type::Ref(t) | Type::RefMut { before: t, .. } => {
@@ -1838,7 +1847,7 @@ impl Context {
                 }
             }
             Type::FreeVar(fv) => {
-                let sup = fv.get_sup().unwrap();
+                let sup = fv.get_super().unwrap();
                 if let Some(res) = self.get_mut_nominal_type_ctx(&sup) {
                     return Some(res);
                 }
@@ -2215,7 +2224,7 @@ impl Context {
         #[allow(clippy::single_match)]
         match lhs {
             Type::FreeVar(fv) => {
-                if let Some(sup) = fv.get_sup() {
+                if let Some(sup) = fv.get_super() {
                     let insts = self.get_trait_impls(&sup);
                     let candidates = insts.into_iter().filter_map(move |inst| {
                         if self.supertype_of(&inst.sup_trait, &sup) {
@@ -2251,7 +2260,7 @@ impl Context {
             Type::Refinement(refine) => self.is_class(&refine.t),
             Type::Ref(t) | Type::RefMut { before: t, .. } => self.is_class(t),
             _ => {
-                if let Some(ctx) = self.get_nominal_type_ctx(typ) {
+                if let Some((_, ctx)) = self.get_nominal_type_ctx(typ) {
                     ctx.kind.is_class()
                 } else {
                     // TODO: unknown types
@@ -2274,7 +2283,7 @@ impl Context {
             Type::Refinement(refine) => self.is_trait(&refine.t),
             Type::Ref(t) | Type::RefMut { before: t, .. } => self.is_trait(t),
             _ => {
-                if let Some(ctx) = self.get_nominal_type_ctx(typ) {
+                if let Some((_, ctx)) = self.get_nominal_type_ctx(typ) {
                     ctx.kind.is_trait()
                 } else {
                     false
diff --git a/compiler/erg_compiler/context/mod.rs b/compiler/erg_compiler/context/mod.rs
index 8709ec75..d5c98941 100644
--- a/compiler/erg_compiler/context/mod.rs
+++ b/compiler/erg_compiler/context/mod.rs
@@ -421,7 +421,7 @@ impl ContextProvider for Context {
             .chain(self.methods_list.iter().flat_map(|(_, ctx)| ctx.dir()))
             .collect();
         for sup in self.super_classes.iter() {
-            if let Some(sup_ctx) = self.get_nominal_type_ctx(sup) {
+            if let Some((_, sup_ctx)) = self.get_nominal_type_ctx(sup) {
                 vars.extend(sup_ctx.type_dir());
             }
         }
@@ -437,7 +437,7 @@ impl ContextProvider for Context {
         self.get_mod(receiver_name)
             .or_else(|| {
                 let (_, vi) = self.get_var_info(receiver_name)?;
-                self.get_nominal_type_ctx(&vi.t)
+                self.get_nominal_type_ctx(&vi.t).map(|(_, ctx)| ctx)
             })
             .or_else(|| self.rec_get_type(receiver_name).map(|(_, ctx)| ctx))
     }
@@ -1002,6 +1002,12 @@ impl Context {
         self.kind = kind;
     }
 
+    pub(crate) fn clear_invalid_vars(&mut self) {
+        self.locals.retain(|_, v| v.t != Failure);
+        self.decls.retain(|_, v| v.t != Failure);
+        self.params.retain(|(_, v)| v.t != Failure);
+    }
+
     pub fn pop(&mut self) -> Context {
         if let Some(parent) = self.outer.as_mut() {
             let parent = mem::take(parent);
diff --git a/compiler/erg_compiler/context/register.rs b/compiler/erg_compiler/context/register.rs
index ef1a2ffc..494b5fa7 100644
--- a/compiler/erg_compiler/context/register.rs
+++ b/compiler/erg_compiler/context/register.rs
@@ -847,7 +847,7 @@ impl Context {
                         self.level,
                     );
                     for sup in super_classes.into_iter() {
-                        let sup_ctx = self
+                        let (_, sup_ctx) = self
                             .get_nominal_type_ctx(&sup)
                             .unwrap_or_else(|| todo!("{sup} not found"));
                         ctx.register_superclass(sup, sup_ctx);
@@ -965,7 +965,7 @@ impl Context {
                         }
                     }
                     for sup in super_classes.into_iter() {
-                        let sup_ctx = self.get_nominal_type_ctx(&sup).unwrap();
+                        let (_, sup_ctx) = self.get_nominal_type_ctx(&sup).unwrap();
                         ctx.register_supertrait(sup, sup_ctx);
                     }
                     self.register_gen_mono_type(ident, gen, ctx, Const);
diff --git a/compiler/erg_compiler/context/tyvar.rs b/compiler/erg_compiler/context/tyvar.rs
index 30e79d48..4c5880c2 100644
--- a/compiler/erg_compiler/context/tyvar.rs
+++ b/compiler/erg_compiler/context/tyvar.rs
@@ -5,7 +5,9 @@ use std::option::Option;
 use erg_common::error::Location;
 use erg_common::traits::{Locational, Stream};
 use erg_common::Str;
-use erg_common::{assume_unreachable, fn_name, log};
+use erg_common::{assume_unreachable, fn_name};
+#[allow(unused_imports)]
+use erg_common::{fmt_vec, log};
 
 use crate::ty::constructors::*;
 use crate::ty::free::{Constraint, FreeKind, HasLevel};
@@ -422,7 +424,7 @@ impl Context {
             }
             Type::Poly { name, mut params } => {
                 let typ = poly(&name, params.clone());
-                let ctx = self.get_nominal_type_ctx(&typ).unwrap();
+                let (_, ctx) = self.get_nominal_type_ctx(&typ).unwrap();
                 let variances = ctx.type_params_variance();
                 for (param, variance) in params.iter_mut().zip(variances.into_iter()) {
                     *param = self.deref_tp(mem::take(param), variance, loc)?;
@@ -1511,63 +1513,86 @@ impl Context {
                 },
             ) => {
                 // e.g. Set(?T) <: Eq(Set(?T))
+                //      Array(Str) <: Iterable(Str)
                 if ln != rn {
-                    if let Some(sub_ctx) = self.get_nominal_type_ctx(maybe_sub) {
+                    if let Some((sub_def_t, sub_ctx)) = self.get_nominal_type_ctx(maybe_sub) {
+                        self.substitute_typarams(sub_def_t, maybe_sub);
                         for sup_trait in sub_ctx.super_traits.iter() {
                             if self.supertype_of(maybe_sup, sup_trait) {
                                 for (l_maybe_sub, r_maybe_sup) in sup_trait.typarams().iter().zip(rps.iter()) {
-                                    self.sub_unify_tp(l_maybe_sub, r_maybe_sup, None, loc, false)?;
+                                    self.sub_unify_tp(l_maybe_sub, r_maybe_sup, None, loc, false)
+                                        .map_err(|e| { self.undo_substitute_typarams(sub_def_t); e })?;
                                 }
+                                self.undo_substitute_typarams(sub_def_t);
                                 return Ok(());
                             }
                         }
                     }
-                    return Err(TyCheckErrors::from(TyCheckError::unification_error(
+                    Err(TyCheckErrors::from(TyCheckError::unification_error(
                         self.cfg.input.clone(),
                         line!() as usize,
                         maybe_sub,
                         maybe_sup,
                         loc,
                         self.caused_by(),
-                    )));
+                    )))
+                } else {
+                    for (l_maybe_sub, r_maybe_sup) in lps.iter().zip(rps.iter()) {
+                        self.sub_unify_tp(l_maybe_sub, r_maybe_sup, None, loc, false)?;
+                    }
+                    Ok(())
                 }
-                for (l_maybe_sub, r_maybe_sup) in lps.iter().zip(rps.iter()) {
-                    self.sub_unify_tp(l_maybe_sub, r_maybe_sup, None, loc, false)?;
-                }
-                Ok(())
             }
-            (Type::And(l, r), _)
-            | (Type::Or(l, r), _)
-            | (Type::Not(l, r), _) => {
+            // (X or Y) <: Z is valid when X <: Z and Y <: Z
+            (Type::Or(l, r), _) => {
                 self.sub_unify(l, maybe_sup, loc, param_name)?;
-                self.sub_unify(r, maybe_sup, loc, param_name)?;
-                Ok(())
+                self.sub_unify(r, maybe_sup, loc, param_name)
             }
-            (_, Type::And(l, r))
-            | (_, Type::Or(l, r))
-            | (_, Type::Not(l, r)) => {
+            // X <: (Y and Z) is valid when X <: Y and X <: Z
+            (_, Type::And(l, r)) => {
                 self.sub_unify(maybe_sub, l, loc, param_name)?;
-                self.sub_unify(maybe_sub, r, loc, param_name)?;
-                Ok(())
+                self.sub_unify(maybe_sub, r, loc, param_name)
+            }
+            // (X and Y) <: Z is valid when X <: Z or Y <: Z
+            (Type::And(l, r), _) => {
+                self.sub_unify(l, maybe_sup, loc, param_name)
+                    .or_else(|_e| self.sub_unify(r, maybe_sup, loc, param_name))
+            }
+            // X <: (Y or Z) is valid when X <: Y or X <: Z
+            (_, Type::Or(l, r)) => {
+                self.sub_unify(maybe_sub, l, loc, param_name)
+                    .or_else(|_e| self.sub_unify(maybe_sub, r, loc, param_name))
             }
             (_, Type::Ref(t)) => {
-                self.sub_unify(maybe_sub, t, loc, param_name)?;
-                Ok(())
+                self.sub_unify(maybe_sub, t, loc, param_name)
             }
             (_, Type::RefMut{ before, .. }) => {
-                self.sub_unify(maybe_sub, before, loc, param_name)?;
-                Ok(())
+                self.sub_unify(maybe_sub, before, loc, param_name)
             }
             (Type::Proj { .. }, _) => todo!(),
             (_, Type::Proj { .. }) => todo!(),
-            (Refinement(l), Refinement(r)) => {
-                if l.preds.len() == 1 && r.preds.len() == 1 {
-                    let l_first = l.preds.iter().next().unwrap();
-                    let r_first = r.preds.iter().next().unwrap();
-                    self.sub_unify_pred(l_first, r_first, loc)?;
+            // TODO: Judgment for any number of preds
+            (Refinement(sub), Refinement(sup)) => {
+                // {I: Int or Str | I == 0} <: {I: Int}
+                if self.subtype_of(&sub.t, &sup.t) {
+                    self.sub_unify(&sub.t, &sup.t, loc, param_name)?;
+                }
+                if sup.preds.is_empty() {
+                    self.sub_unify(&sub.t, &sup.t, loc, param_name)?;
                     return Ok(());
                 }
-                todo!("{l}, {r}")
+                if sub.preds.len() == 1 && sup.preds.len() == 1 {
+                    let sub_first = sub.preds.iter().next().unwrap();
+                    let sup_first = sup.preds.iter().next().unwrap();
+                    self.sub_unify_pred(sub_first, sup_first, loc)?;
+                    return Ok(());
+                }
+                todo!("{sub}, {sup}")
+            },
+            // {I: Int | I >= 1} <: Nat == {I: Int | I >= 0}
+            (Type::Refinement(_), sup) => {
+                let sup = self.into_refinement(sup.clone());
+                self.sub_unify(maybe_sub, &Type::Refinement(sup), loc, param_name)
             },
             (Type::Subr(_) | Type::Record(_), Type) => Ok(()),
             // REVIEW: correct?
diff --git a/compiler/erg_compiler/error.rs b/compiler/erg_compiler/error.rs
index 471b6195..52f6f1c0 100644
--- a/compiler/erg_compiler/error.rs
+++ b/compiler/erg_compiler/error.rs
@@ -554,6 +554,79 @@ impl TyCheckError {
         )
     }
 
+    pub fn param_error(
+        input: Input,
+        errno: usize,
+        loc: Location,
+        caused_by: String,
+        expect: usize,
+        found: usize,
+    ) -> Self {
+        let mut expct = StyledStrings::default();
+        switch_lang!(
+            "japanese" => expct.push_str("予期した個数: "),
+            "simplified_chinese" =>expct.push_str("预期: "),
+            "traditional_chinese" => expct.push_str("預期: "),
+            "english" => expct.push_str("expected: "),
+        );
+        expct.push_str_with_color_and_attribute(format!("{}", expect), HINT, ATTR);
+
+        let mut fnd = StyledStrings::default();
+        switch_lang!(
+            "japanese" => fnd.push_str("与えられた個数: "),
+            "simplified_chinese" => fnd.push_str("但找到: "),
+            "traditional_chinese" => fnd.push_str("但找到: "),
+            "english" =>fnd.push_str("but found: "),
+        );
+        fnd.push_str_with_color_and_attribute(format!("{}", found), ERR, ATTR);
+
+        Self::new(
+            ErrorCore::new(
+                vec![SubMessage::ambiguous_new(
+                    loc,
+                    vec![expct.to_string(), fnd.to_string()],
+                    None,
+                )],
+                switch_lang!(
+                    "japanese" => format!("引数の数が違います"),
+                    "simplified_chinese" => format!("参数的数量不匹配"),
+                    "traditional_chinese" => format!("參數的數量不匹配"),
+                    "english" => format!("the number of parameters is mismatched"),
+                ),
+                errno,
+                TypeError,
+                loc,
+            ),
+            input,
+            caused_by,
+        )
+    }
+
+    pub fn default_param_error(
+        input: Input,
+        errno: usize,
+        loc: Location,
+        caused_by: String,
+        name: &str,
+    ) -> Self {
+        Self::new(
+            ErrorCore::new(
+                vec![],
+                switch_lang!(
+                    "japanese" => format!("{name}はデフォルト引数を受け取りません"),
+                    "simplified_chinese" => format!("{name}不接受默认参数"),
+                    "traditional_chinese" => format!("{name}不接受預設參數"),
+                    "english" => format!("{name} does not accept default parameters"),
+                ),
+                errno,
+                TypeError,
+                loc,
+            ),
+            input,
+            caused_by,
+        )
+    }
+
     pub fn match_error(
         input: Input,
         errno: usize,
diff --git a/compiler/erg_compiler/hir.rs b/compiler/erg_compiler/hir.rs
index b1562dc8..45700145 100644
--- a/compiler/erg_compiler/hir.rs
+++ b/compiler/erg_compiler/hir.rs
@@ -1967,6 +1967,11 @@ impl Expr {
         }
     }
 
+    pub fn to_string_notype(&self) -> String {
+        let s = self.to_string();
+        s.split("(:").next().unwrap_or("?").trim_end().to_string()
+    }
+
     /// 参照するオブジェクト自体が持っている名前(e.g. Int.qual_name == Some("int"), Socket!.qual_name == Some("io.Socket!"))
     pub fn qual_name(&self) -> Option<&str> {
         match self {
diff --git a/compiler/erg_compiler/lib/pystd/re.d.er b/compiler/erg_compiler/lib/pystd/re.d.er
index 98515c8a..42cbd566 100644
--- a/compiler/erg_compiler/lib/pystd/re.d.er
+++ b/compiler/erg_compiler/lib/pystd/re.d.er
@@ -1 +1,48 @@
-.sub: (pattern: Str, repl: Str, string: Str, count := Nat) -> Str
+.RegexFlag: ClassType
+.A: .RegexFlag
+.ASCII: .RegexFlag
+.DEBUG: .RegexFlag
+.I: .RegexFlag
+.IGNORECASE: .RegexFlag
+.L: .RegexFlag
+.LOCALE: .RegexFlag
+.M: .RegexFlag
+.MULTILINE: .RegexFlag
+.NOFLAG: .RegexFlag
+.S: .RegexFlag
+.DOTALL: .RegexFlag
+.X: .RegexFlag
+.VERBOSE: .RegexFlag
+
+.Match: ClassType
+.Match.expand: (self: .Match, template: Str) -> Str
+# TODO: tuple
+.Match.group: (self: .Match, x := Int or Str) -> Str
+.Match.__getitem__: (self: .Match, x := Int or Str) -> Str
+
+.Pattern: ClassType
+.Pattern.search: (self: .Pattern, string: Str) -> .Match or NoneType
+.Pattern.match: (self: .Pattern, string: Str) -> .Match or NoneType
+.Pattern.fullmatch: (self: .Pattern, string: Str) -> .Match or NoneType
+.Pattern.split: (self: .Pattern, string: Str, maxspilit := Nat) -> [Str; _]
+.Pattern.findall: (self: .Pattern, string: Str) -> [Str; _]
+# TODO: iterator
+.Pattern.finditer: (self: .Pattern, string: Str) -> [.Match; _]
+.Pattern.sub: (self: .Pattern, repl: Str, string: Str, count := Nat) -> Str
+.Pattern.subn: (self: .Pattern, repl: Str, string: Str, count := Nat) -> (Str, Nat)
+.Pattern.flags: Nat
+.Pattern.groups: Nat
+.Pattern.pattern: Str
+
+.compile: (pattern: Str, flags := Nat or .RegexFlag) -> .Pattern
+.search: (pattern: Str, string: Str, flags := Nat or .RegexFlag) -> .Match or NoneType
+.match: (pattern: Str, string: Str, flags := Nat or .RegexFlag) -> .Match or NoneType
+.fullmatch: (pattern: Str, string: Str, flags := Nat or .RegexFlag) -> .Match or NoneType
+.split: (pattern: Str, string: Str, maxspilit := Nat, flags := Nat or .RegexFlag) -> [Str; _]
+.findall: (pattern: Str, string: Str, flags := Nat or .RegexFlag) -> [Str; _]
+# TODO: iterator
+.finditer: (pattern: Str, string: Str, flags := Nat or .RegexFlag) -> [.Match; _]
+.sub: (pattern: Str, repl: Str, string: Str, count := Nat, flags := Nat or .RegexFlag) -> Str
+.subn: (pattern: Str, repl: Str, string: Str, count := Nat, flags := Nat or .RegexFlag) -> (Str, Nat)
+.escape: (pattern: Str) -> Str
+.purge!: () => ()
diff --git a/compiler/erg_compiler/lib/std/_erg_int.py b/compiler/erg_compiler/lib/std/_erg_int.py
new file mode 100644
index 00000000..78b0e413
--- /dev/null
+++ b/compiler/erg_compiler/lib/std/_erg_int.py
@@ -0,0 +1,85 @@
+from _erg_result import Error
+
+class Int(int):
+    def try_new(i): # -> Result[Nat]
+        if isinstance(i, int):
+            Int(i)
+        else:
+            Error("not an integer")
+    def succ(self):
+        return Int(self + 1)
+    def pred(self):
+        return Int(self - 1)
+    def mutate(self):
+        return IntMut(self)
+
+class IntMut(): # inherits Int
+    value: Int
+
+    def __init__(self, i):
+        self.value = Int(i)
+    def __repr__(self):
+        return self.value.__repr__()
+    def __eq__(self, other):
+        if isinstance(other, Int):
+            return self.value == other
+        else:
+            return self.value == other.value
+    def __ne__(self, other):
+        if isinstance(other, Int):
+            return self.value != other
+        else:
+            return self.value != other.value
+    def __le__(self, other):
+        if isinstance(other, Int):
+            return self.value <= other
+        else:
+            return self.value <= other.value
+    def __ge__(self, other):
+        if isinstance(other, Int):
+            return self.value >= other
+        else:
+            return self.value >= other.value
+    def __lt__(self, other):
+        if isinstance(other, Int):
+            return self.value < other
+        else:
+            return self.value < other.value
+    def __gt__(self, other):
+        if isinstance(other, Int):
+            return self.value > other
+        else:
+            return self.value > other.value
+    def __add__(self, other):
+        if isinstance(other, Int):
+            return IntMut(self.value + other)
+        else:
+            return IntMut(self.value + other.value)
+    def __sub__(self, other):
+        if isinstance(other, Int):
+            return IntMut(self.value - other)
+        else:
+            return IntMut(self.value - other.value)
+    def __mul__(self, other):
+        if isinstance(other, Int):
+            return IntMut(self.value * other)
+        else:
+            return IntMut(self.value * other.value)
+    def __floordiv__(self, other):
+        if isinstance(other, Int):
+            return IntMut(self.value // other)
+        else:
+            return IntMut(self.value // other.value)
+    def __pow__(self, other):
+        if isinstance(other, Int):
+            return IntMut(self.value ** other)
+        else:
+            return IntMut(self.value ** other.value)
+    def inc(self, i=1):
+        self.value = Int(self.value + i)
+    def dec(self, i=1):
+        self.value = Int(self.value - i)
+    def succ(self):
+        return self.value.succ()
+    def pred(self):
+        return self.value.pred()
diff --git a/compiler/erg_compiler/lib/std/_erg_mutate_operator.py b/compiler/erg_compiler/lib/std/_erg_mutate_operator.py
new file mode 100644
index 00000000..e5753140
--- /dev/null
+++ b/compiler/erg_compiler/lib/std/_erg_mutate_operator.py
@@ -0,0 +1,5 @@
+def mutate_operator(x):
+    if hasattr(x, 'mutate'):
+        return x.mutate()
+    else:
+        return x
diff --git a/compiler/erg_compiler/lib/std/_erg_nat.py b/compiler/erg_compiler/lib/std/_erg_nat.py
index f13e0820..4cadd671 100644
--- a/compiler/erg_compiler/lib/std/_erg_nat.py
+++ b/compiler/erg_compiler/lib/std/_erg_nat.py
@@ -1,6 +1,8 @@
 from _erg_result import Error
+from _erg_int import Int
+from _erg_int import IntMut
 
-class Nat(int):
+class Nat(Int):
     def try_new(i): # -> Result[Nat]
         if i >= 0:
             return Nat(i)
@@ -16,3 +18,67 @@ class Nat(int):
             return self - other
         else:
             return 0
+    def mutate(self):
+        return NatMut(self)
+
+class NatMut(IntMut): # and Nat
+    value: Nat
+
+    def __init__(self, n):
+        self.value = n
+    def __repr__(self):
+        return self.value.__repr__()
+    def __eq__(self, other):
+        if isinstance(other, Int):
+            return self.value == other
+        else:
+            return self.value == other.value
+    def __ne__(self, other):
+        if isinstance(other, Int):
+            return self.value != other
+        else:
+            return self.value != other.value
+    def __le__(self, other):
+        if isinstance(other, Int):
+            return self.value <= other
+        else:
+            return self.value <= other.value
+    def __ge__(self, other):
+        if isinstance(other, Int):
+            return self.value >= other
+        else:
+            return self.value >= other.value
+    def __lt__(self, other):
+        if isinstance(other, Int):
+            return self.value < other
+        else:
+            return self.value < other.value
+    def __gt__(self, other):
+        if isinstance(other, Int):
+            return self.value > other
+        else:
+            return self.value > other.value
+    def __add__(self, other):
+        if isinstance(other, Nat):
+            return NatMut(self.value + other)
+        else:
+            return NatMut(self.value + other.value)
+    def __mul__(self, other):
+        if isinstance(other, Nat):
+            return NatMut(self.value * other)
+        else:
+            return NatMut(self.value * other.value)
+    def __pow__(self, other):
+        if isinstance(other, Nat):
+            return NatMut(self.value ** other)
+        else:
+            return NatMut(self.value ** other.value)
+    def try_new(i): # -> Result[Nat]
+        if i >= 0:
+            return NatMut(i)
+        else:
+            return Error("Nat can't be negative")
+
+    def times(self, f):
+        for _ in range(self.value):
+            f()
diff --git a/compiler/erg_compiler/lib/std/_erg_range.py b/compiler/erg_compiler/lib/std/_erg_range.py
index 6a0914d5..933958dd 100644
--- a/compiler/erg_compiler/lib/std/_erg_range.py
+++ b/compiler/erg_compiler/lib/std/_erg_range.py
@@ -69,7 +69,7 @@ class RangeIterator:
                 self.needle = chr(ord(self.needle) + 1)
         else:
             if not(self.needle in self.rng):
-                self.needle = self.needle.incremented()
+                self.needle = self.needle.succ()
 
     def __iter__(self):
         return self
@@ -88,7 +88,7 @@ class RangeIterator:
         else:
             if self.needle in self.rng:
                 result = self.needle
-                self.needle = self.needle.incremented()
+                self.needle = self.needle.succ()
                 return result
         raise StopIteration
 
diff --git a/compiler/erg_compiler/lib/std/_erg_std_prelude.py b/compiler/erg_compiler/lib/std/_erg_std_prelude.py
index c7664816..47c65d1c 100644
--- a/compiler/erg_compiler/lib/std/_erg_std_prelude.py
+++ b/compiler/erg_compiler/lib/std/_erg_std_prelude.py
@@ -1,7 +1,9 @@
 from _erg_range import Range, LeftOpenRange, RightOpenRange, OpenRange, ClosedRange, RangeIterator
 from _erg_result import Result, Error, is_ok
-from _erg_nat import Nat
+from _erg_int import Int, IntMut
+from _erg_nat import Nat, NatMut
 from _erg_bool import Bool
-from _erg_str import Str
+from _erg_str import Str, StrMut
 from _erg_array import Array
 from _erg_in_operator import in_operator
+from _erg_mutate_operator import mutate_operator
diff --git a/compiler/erg_compiler/lib/std/_erg_std_prelude_old.py b/compiler/erg_compiler/lib/std/_erg_std_prelude_old.py
index ec67f54a..b8a17aff 100644
--- a/compiler/erg_compiler/lib/std/_erg_std_prelude_old.py
+++ b/compiler/erg_compiler/lib/std/_erg_std_prelude_old.py
@@ -54,7 +54,6 @@ class Bool(Nat):
 
 class Str(str):
     def __instancecheck__(cls, obj):
-        print(cls, obj)
         return obj == Str or obj == str
 
     def try_new(s: str): # -> Result[Nat]
diff --git a/compiler/erg_compiler/lib/std/_erg_str.py b/compiler/erg_compiler/lib/std/_erg_str.py
index 6d278376..183015eb 100644
--- a/compiler/erg_compiler/lib/std/_erg_str.py
+++ b/compiler/erg_compiler/lib/std/_erg_str.py
@@ -13,27 +13,47 @@ class Str(str):
             return Str(self[i])
         else:
             return None
+    def mutate(self):
+        return StrMut(self)
 
-class StrMut(Str):
+class StrMut(): # Inherits Str
+    value: Str
+
+    def __init__(self, s: str):
+        self.value = s
+    def __repr__(self):
+        return self.value.__repr__()
+    def __eq__(self, other):
+        if isinstance(other, Str):
+            return self.value == other
+        else:
+            return self.value == other.value
+    def __ne__(self, other):
+        if isinstance(other, Str):
+            return self.value != other
+        else:
+            return self.value != other.value
     def try_new(s: str):
         if isinstance(s, str):
-            return StrMut(s)
+            self = StrMut()
+            self.value = s
+            return self
         else:
             return Error("Str! can't be other than str")
     def clear(self):
-        self = ""
+        self.value = ""
     def pop(self):
-        if len(self) > 0:
-            last = self[-1]
-            self = self[:-1]
+        if len(self.value) > 0:
+            last = self.value[-1]
+            self.value = self.value[:-1]
             return last
         else:
             return Error("Can't pop from empty `Str!`")
     def push(self, c: str):
-        self += c
+        self.value += c
     def remove(self, idx: int):
-        char = self[idx]
-        self = self[:idx] + self[idx+1:]
+        char = self.value[idx]
+        self.value = self.value[:idx] + self.value[idx+1:]
         return char
     def insert(self, idx: int, c: str):
-        self = self[:idx] + c + self[idx:]
+        self.value = self.value[:idx] + c + self.value[idx:]
diff --git a/compiler/erg_compiler/lower.rs b/compiler/erg_compiler/lower.rs
index 1e203c78..9f051920 100644
--- a/compiler/erg_compiler/lower.rs
+++ b/compiler/erg_compiler/lower.rs
@@ -309,6 +309,31 @@ impl ASTLowerer {
         }
     }
 
+    fn elem_err(&self, l: &Type, r: &Type, elem: &hir::Expr) -> LowerErrors {
+        let elem_disp_notype = elem.to_string_notype();
+        let l = Context::readable_type(l);
+        let r = Context::readable_type(r);
+        LowerErrors::from(LowerError::syntax_error(
+            self.cfg.input.clone(),
+            line!() as usize,
+            elem.loc(),
+            String::from(&self.ctx.name[..]),
+            switch_lang!(
+                "japanese" => "配列の要素は全て同じ型である必要があります",
+                "simplified_chinese" => "数组元素必须全部是相同类型",
+                "traditional_chinese" => "數組元素必須全部是相同類型",
+                "english" => "all elements of an array must be of the same type",
+            )
+            .to_owned(),
+            Some(switch_lang!(
+                "japanese" => format!("[..., {elem_disp_notype}: {l} or {r}]など明示的に型を指定してください"),
+                "simplified_chinese" => format!("请明确指定类型，例如: [..., {elem_disp_notype}: {l} or {r}]"),
+                "traditional_chinese" => format!("請明確指定類型，例如: [..., {elem_disp_notype}: {l} or {r}]"),
+                "english" => format!("please specify the type explicitly, e.g. [..., {elem_disp_notype}: {l} or {r}]"),
+            )),
+        ))
+    }
+
     fn lower_normal_array(&mut self, array: ast::NormalArray) -> LowerResult<hir::NormalArray> {
         log!(info "entered {}({array})", fn_name!());
         let mut new_array = vec![];
@@ -317,29 +342,16 @@ impl ASTLowerer {
         for elem in elems {
             let elem = self.lower_expr(elem.expr)?;
             union = self.ctx.union(&union, elem.ref_t());
-            if matches!(union, Type::Or(_, _)) {
-                return Err(LowerErrors::from(LowerError::syntax_error(
-                    self.cfg.input.clone(),
-                    line!() as usize,
-                    elem.loc(),
-                    String::from(&self.ctx.name[..]),
-                    switch_lang!(
-                        "japanese" => "配列の要素は全て同じ型である必要があります",
-                        "simplified_chinese" => "数组元素必须全部是相同类型",
-                        "traditional_chinese" => "數組元素必須全部是相同類型",
-                        "english" => "all elements of an array must be of the same type",
-                    )
-                    .to_owned(),
-                    Some(
-                        switch_lang!(
-                            "japanese" => "Int or Strなど明示的に型を指定してください",
-                            "simplified_chinese" => "请明确指定类型，例如: Int or Str",
-                            "traditional_chinese" => "請明確指定類型，例如: Int or Str",
-                            "english" => "please specify the type explicitly, e.g. Int or Str",
-                        )
-                        .to_owned(),
-                    ),
-                )));
+            if let Some((l, r)) = union.union_types() {
+                match (l.is_unbound_var(), r.is_unbound_var()) {
+                    (false, false) => {
+                        return Err(self.elem_err(&l, &r, &elem));
+                    }
+                    // TODO: check if the type is compatible with the other type
+                    (true, false) => {}
+                    (false, true) => {}
+                    (true, true) => {}
+                }
             }
             new_array.push(elem);
         }
@@ -1209,7 +1221,7 @@ impl ASTLowerer {
             if let Some((trait_, trait_loc)) = &impl_trait {
                 self.register_trait_impl(&class, trait_, *trait_loc)?;
             }
-            if let Some(class_root) = self.ctx.get_nominal_type_ctx(&class) {
+            if let Some((_, class_root)) = self.ctx.get_nominal_type_ctx(&class) {
                 if !class_root.kind.is_class() {
                     return Err(LowerErrors::from(LowerError::method_definition_error(
                         self.cfg.input.clone(),
@@ -1278,7 +1290,7 @@ impl ASTLowerer {
             self.check_collision_and_push(class);
         }
         let class = mono(hir_def.sig.ident().inspect());
-        let class_ctx = self.ctx.get_nominal_type_ctx(&class).unwrap();
+        let (_, class_ctx) = self.ctx.get_nominal_type_ctx(&class).unwrap();
         let type_obj = enum_unwrap!(self.ctx.rec_get_const_obj(hir_def.sig.ident().inspect()).unwrap(), ValueObj::Type:(TypeObj::Generated:(_)));
         let sup_type = enum_unwrap!(&hir_def.body.block.first().unwrap(), hir::Expr::Call)
             .args
@@ -1385,7 +1397,7 @@ impl ASTLowerer {
                 set! {TypeRelationInstance::new(class.clone(), trait_.clone())},
             );
         }
-        let trait_ctx = if let Some(trait_ctx) = self.ctx.get_nominal_type_ctx(trait_) {
+        let trait_ctx = if let Some((_, trait_ctx)) = self.ctx.get_nominal_type_ctx(trait_) {
             trait_ctx.clone()
         } else {
             // TODO: maybe parameters are wrong
@@ -1523,7 +1535,7 @@ impl ASTLowerer {
                             other => todo!("{other}"),
                         },
                         TypeObj::Builtin(_typ) => {
-                            let ctx = self.ctx.get_nominal_type_ctx(_typ).unwrap();
+                            let (_, ctx) = self.ctx.get_nominal_type_ctx(_typ).unwrap();
                             for (decl_name, decl_vi) in ctx.decls.iter() {
                                 if let Some((name, vi)) = self.ctx.get_local_kv(decl_name.inspect())
                                 {
@@ -2079,6 +2091,7 @@ impl ASTLowerer {
                 }
             }
         }
+        self.ctx.clear_invalid_vars();
         self.ctx.check_decls().unwrap_or_else(|mut errs| {
             self.errs.append(&mut errs);
         });
diff --git a/compiler/erg_compiler/transpile.rs b/compiler/erg_compiler/transpile.rs
index 607c9603..fef8e10e 100644
--- a/compiler/erg_compiler/transpile.rs
+++ b/compiler/erg_compiler/transpile.rs
@@ -209,6 +209,7 @@ pub struct ScriptGenerator {
     level: usize,
     fresh_var_n: usize,
     namedtuple_loaded: bool,
+    mutate_op_loaded: bool,
     in_op_loaded: bool,
     range_ops_loaded: bool,
     builtin_types_loaded: bool,
@@ -221,6 +222,7 @@ impl ScriptGenerator {
             level: 0,
             fresh_var_n: 0,
             namedtuple_loaded: false,
+            mutate_op_loaded: false,
             in_op_loaded: false,
             range_ops_loaded: false,
             builtin_types_loaded: false,
@@ -244,12 +246,14 @@ impl ScriptGenerator {
     // TODO: more smart way
     fn replace_import(src: &str) -> String {
         src.replace("from _erg_nat import Nat", "")
-            .replace("from _erg_result import Error", "")
-            .replace("from _erg_result import is_ok", "")
+            .replace("from _erg_int import IntMut", "")
+            .replace("from _erg_int import Int", "")
             .replace("from _erg_bool import Bool", "")
             .replace("from _erg_str import Str", "")
             .replace("from _erg_array import Array", "")
             .replace("from _erg_range import Range", "")
+            .replace("from _erg_result import Error", "")
+            .replace("from _erg_result import is_ok", "")
     }
 
     fn load_namedtuple(&mut self) {
@@ -259,6 +263,7 @@ impl ScriptGenerator {
     // TODO: name escaping
     fn load_range_ops(&mut self) {
         self.prelude += &Self::replace_import(include_str!("lib/std/_erg_result.py"));
+        self.prelude += &Self::replace_import(include_str!("lib/std/_erg_int.py"));
         self.prelude += &Self::replace_import(include_str!("lib/std/_erg_nat.py"));
         self.prelude += &Self::replace_import(include_str!("lib/std/_erg_str.py"));
         self.prelude += &Self::replace_import(include_str!("lib/std/_erg_range.py"));
@@ -270,16 +275,22 @@ impl ScriptGenerator {
         self.prelude += &Self::replace_import(include_str!("lib/std/_erg_in_operator.py"));
     }
 
+    fn load_mutate_op(&mut self) {
+        self.prelude += &Self::replace_import(include_str!("lib/std/_erg_mutate_operator.py"));
+    }
+
     fn load_builtin_types(&mut self) {
         if self.range_ops_loaded {
             self.prelude += &Self::replace_import(include_str!("lib/std/_erg_array.py"));
         } else if self.in_op_loaded {
+            self.prelude += &Self::replace_import(include_str!("lib/std/_erg_int.py"));
             self.prelude += &Self::replace_import(include_str!("lib/std/_erg_nat.py"));
             self.prelude += &Self::replace_import(include_str!("lib/std/_erg_bool.py"));
             self.prelude += &Self::replace_import(include_str!("lib/std/_erg_str.py"));
             self.prelude += &Self::replace_import(include_str!("lib/std/_erg_array.py"));
         } else {
             self.prelude += &Self::replace_import(include_str!("lib/std/_erg_result.py"));
+            self.prelude += &Self::replace_import(include_str!("lib/std/_erg_int.py"));
             self.prelude += &Self::replace_import(include_str!("lib/std/_erg_nat.py"));
             self.prelude += &Self::replace_import(include_str!("lib/std/_erg_bool.py"));
             self.prelude += &Self::replace_import(include_str!("lib/std/_erg_str.py"));
@@ -289,12 +300,32 @@ impl ScriptGenerator {
 
     fn transpile_expr(&mut self, expr: Expr) -> String {
         match expr {
-            Expr::Lit(lit) => lit.token.content.to_string(),
+            Expr::Lit(lit) => {
+                if matches!(
+                    &lit.value,
+                    ValueObj::Bool(_) | ValueObj::Int(_) | ValueObj::Nat(_) | ValueObj::Str(_)
+                ) {
+                    if !self.builtin_types_loaded {
+                        self.load_builtin_types();
+                        self.builtin_types_loaded = true;
+                    }
+                    format!("{}({})", lit.value.class(), lit.token.content)
+                } else {
+                    lit.token.content.to_string()
+                }
+            }
             Expr::Call(call) => self.transpile_call(call),
             Expr::BinOp(bin) => self.transpile_binop(bin),
             Expr::UnaryOp(unary) => {
-                let mut code = "(".to_string();
-                if unary.op.kind != TokenKind::Mutate {
+                let mut code = "".to_string();
+                if unary.op.kind == TokenKind::Mutate {
+                    if !self.mutate_op_loaded {
+                        self.load_mutate_op();
+                        self.mutate_op_loaded = true;
+                    }
+                    code += "mutate_operator(";
+                } else {
+                    code += "(";
                     code += &unary.op.content;
                 }
                 code += &self.transpile_expr(*unary.expr);
@@ -681,8 +712,16 @@ impl ScriptGenerator {
     fn transpile_params(&mut self, params: Params) -> String {
         let mut code = String::new();
         for non_default in params.non_defaults {
-            let ParamPattern::VarName(param) = non_default.pat else { todo!() };
-            code += &format!("{}__,", param.into_token().content);
+            match non_default.pat {
+                ParamPattern::VarName(param) => {
+                    code += &format!("{}__,", param.into_token().content);
+                }
+                ParamPattern::Discard(_) => {
+                    code += &format!("_{},", self.fresh_var_n);
+                    self.fresh_var_n += 1;
+                }
+                _ => unreachable!(),
+            }
         }
         for default in params.defaults {
             let ParamPattern::VarName(param) = default.sig.pat else { todo!() };
diff --git a/compiler/erg_compiler/ty/free.rs b/compiler/erg_compiler/ty/free.rs
index c1aaf2ac..cc7da214 100644
--- a/compiler/erg_compiler/ty/free.rs
+++ b/compiler/erg_compiler/ty/free.rs
@@ -152,6 +152,7 @@ impl Constraint {
         }
     }
 
+    /// :> Sub
     pub fn get_sub(&self) -> Option<&Type> {
         match self {
             Self::Sandwiched { sub, .. } => Some(sub),
@@ -159,6 +160,7 @@ impl Constraint {
         }
     }
 
+    /// <: Sup
     pub fn get_super(&self) -> Option<&Type> {
         match self {
             Self::Sandwiched { sup, .. } => Some(sup),
@@ -567,10 +569,12 @@ impl<T: CanbeFree> Free<T> {
         self.constraint().and_then(|c| c.get_type().cloned())
     }
 
-    pub fn get_sup(&self) -> Option<Type> {
+    /// <: Super
+    pub fn get_super(&self) -> Option<Type> {
         self.constraint().and_then(|c| c.get_super().cloned())
     }
 
+    /// :> Sub
     pub fn get_sub(&self) -> Option<Type> {
         self.constraint().and_then(|c| c.get_sub().cloned())
     }
diff --git a/compiler/erg_compiler/ty/mod.rs b/compiler/erg_compiler/ty/mod.rs
index 1ddf638a..4066dcba 100644
--- a/compiler/erg_compiler/ty/mod.rs
+++ b/compiler/erg_compiler/ty/mod.rs
@@ -2043,6 +2043,24 @@ impl Type {
         }
     }
 
+    pub fn container_len(&self) -> Option<usize> {
+        log!(err "{self}");
+        match self {
+            Self::Poly { name, params } => match &name[..] {
+                "Array" => {
+                    if let TyParam::Value(ValueObj::Nat(n)) = &params[0] {
+                        Some(*n as usize)
+                    } else {
+                        None
+                    }
+                }
+                "Tuple" => Some(params.len()),
+                _ => None,
+            },
+            _ => None,
+        }
+    }
+
     pub fn typarams(&self) -> Vec<TyParam> {
         match self {
             Self::FreeVar(f) if f.is_linked() => f.crack().typarams(),
diff --git a/compiler/erg_compiler/ty/value.rs b/compiler/erg_compiler/ty/value.rs
index 3dd3c72d..44088e5a 100644
--- a/compiler/erg_compiler/ty/value.rs
+++ b/compiler/erg_compiler/ty/value.rs
@@ -23,6 +23,8 @@ use erg_parser::ast::{ConstArgs, ConstExpr};
 
 use crate::context::eval::type_from_token_kind;
 
+use self::value_set::inner_class;
+
 use super::codeobj::CodeObj;
 use super::constructors::{array_t, dict_t, mono, poly, refinement, set_t, tuple_t};
 use super::typaram::TyParam;
@@ -651,6 +653,14 @@ impl ValueObj {
         }
     }
 
+    pub fn is_int(&self) -> bool {
+        match self {
+            Self::Int(_) | Self::Nat(_) | Self::Bool(_) => true,
+            Self::Mut(n) => n.borrow().is_nat(),
+            _ => false,
+        }
+    }
+
     pub fn is_nat(&self) -> bool {
         match self {
             Self::Nat(_) | Self::Bool(_) => true,
@@ -763,15 +773,21 @@ impl ValueObj {
         }
     }
 
+    pub fn from_const_expr(expr: ConstExpr) -> Self {
+        let ConstExpr::Lit(lit) = expr else { todo!() };
+        let t = type_from_token_kind(lit.token.kind);
+        ValueObj::from_str(t, lit.token.content).unwrap()
+    }
+
+    pub fn tuple_from_const_args(args: ConstArgs) -> Self {
+        Self::Tuple(Rc::from(&Self::vec_from_const_args(args)[..]))
+    }
+
     pub fn vec_from_const_args(args: ConstArgs) -> Vec<Self> {
         args.deconstruct()
             .0
             .into_iter()
-            .map(|elem| {
-                let ConstExpr::Lit(lit) = elem.expr else { todo!() };
-                let t = type_from_token_kind(lit.token.kind);
-                ValueObj::from_str(t, lit.token.content).unwrap()
-            })
+            .map(|elem| Self::from_const_expr(elem.expr))
             .collect::<Vec<_>>()
     }
 
@@ -782,9 +798,12 @@ impl ValueObj {
             Self::Float(_) => Type::Float,
             Self::Str(_) => Type::Str,
             Self::Bool(_) => Type::Bool,
-            // TODO: Zero
             Self::Array(arr) => array_t(
-                arr.iter().next().unwrap().class(),
+                // REVIEW: Never?
+                arr.iter()
+                    .next()
+                    .map(|elem| elem.class())
+                    .unwrap_or(Type::Never),
                 TyParam::value(arr.len()),
             ),
             Self::Dict(dict) => {
@@ -794,7 +813,7 @@ impl ValueObj {
                 dict_t(TyParam::Dict(tp.collect()))
             }
             Self::Tuple(tup) => tuple_t(tup.iter().map(|v| v.class()).collect()),
-            Self::Set(st) => set_t(st.iter().next().unwrap().class(), TyParam::value(st.len())),
+            Self::Set(st) => set_t(inner_class(st), TyParam::value(st.len())),
             Self::Code(_) => Type::Code,
             Self::Record(rec) => {
                 Type::Record(rec.iter().map(|(k, v)| (k.clone(), v.class())).collect())
@@ -1206,7 +1225,10 @@ pub mod value_set {
     }
 
     pub fn inner_class(set: &Set<ValueObj>) -> Type {
-        set.iter().next().unwrap().class()
+        set.iter()
+            .next()
+            .map(|elem| elem.class())
+            .unwrap_or(Type::Never)
     }
 
     pub fn max(set: &Set<ValueObj>) -> Option<ValueObj> {
diff --git a/compiler/erg_parser/ast.rs b/compiler/erg_parser/ast.rs
index f78aeb3f..5eb72307 100644
--- a/compiler/erg_parser/ast.rs
+++ b/compiler/erg_parser/ast.rs
@@ -1979,7 +1979,13 @@ impl fmt::Display for TypeSpec {
                 }
                 write!(f, "}}")
             }
-            Self::Enum(elems) => write!(f, "{{{elems}}}"),
+            Self::Enum(elems) => {
+                write!(f, "{{")?;
+                for elem in elems.pos_args() {
+                    write!(f, "{}, ", elem.expr)?;
+                }
+                write!(f, "}}")
+            }
             Self::Interval { op, lhs, rhs } => write!(f, "{lhs}{}{rhs}", op.inspect()),
             Self::Subr(s) => write!(f, "{s}"),
             Self::TypeApp { spec, args } => write!(f, "{spec}{args}"),
diff --git a/compiler/erg_parser/desugar.rs b/compiler/erg_parser/desugar.rs
index 3c043980..08bbe4f2 100644
--- a/compiler/erg_parser/desugar.rs
+++ b/compiler/erg_parser/desugar.rs
@@ -67,8 +67,7 @@ impl Desugarer {
         let kw_args = kw_args
             .into_iter()
             .map(|arg| {
-                let expr = desugar(arg.expr);
-                KwArg::new(arg.keyword, arg.t_spec, expr) // TODO: t_spec
+                KwArg::new(arg.keyword, arg.t_spec, desugar(arg.expr)) // TODO: t_spec
             })
             .collect();
         Args::new(pos_args, kw_args, paren)
@@ -1003,6 +1002,17 @@ impl Desugarer {
                 insertion_idx += 1;
                 insertion_idx
             }
+            ParamPattern::Lit(l) => {
+                let lit = l.clone();
+                sig.pat = ParamPattern::Discard(Token::new(
+                    TokenKind::UBar,
+                    "_",
+                    l.ln_begin().unwrap(),
+                    l.col_begin().unwrap(),
+                ));
+                sig.t_spec = Some(TypeSpecWithOp::new(COLON, TypeSpec::enum_t_spec(vec![lit])));
+                insertion_idx
+            }
             _ => insertion_idx,
         }
     }
diff --git a/compiler/erg_parser/parse.rs b/compiler/erg_parser/parse.rs
index 60aad381..2d68a66f 100644
--- a/compiler/erg_parser/parse.rs
+++ b/compiler/erg_parser/parse.rs
@@ -935,22 +935,40 @@ impl Parser {
                 }
                 Some(op) if op.category_is(TC::DefOp) => {
                     let op = self.lpop();
+                    let is_multiline_block = self.cur_is(Newline);
                     let lhs = enum_unwrap!(stack.pop(), Some:(ExprOrOp::Expr:(_)));
                     let sig = self.convert_rhs_to_sig(lhs).map_err(|_| self.stack_dec())?;
                     self.counter.inc();
-                    let block = self.try_reduce_block().map_err(|_| self.stack_dec())?;
+                    let block = if is_multiline_block {
+                        self.try_reduce_block().map_err(|_| self.stack_dec())?
+                    } else {
+                        // precedence: `=` < `,`
+                        let expr = self
+                            .try_reduce_expr(true, false, false, false)
+                            .map_err(|_| self.stack_dec())?;
+                        Block::new(vec![expr])
+                    };
                     let body = DefBody::new(op, block, self.counter);
                     self.level -= 1;
                     return Ok(Expr::Def(Def::new(sig, body)));
                 }
                 Some(op) if op.category_is(TC::LambdaOp) => {
                     let op = self.lpop();
+                    let is_multiline_block = self.cur_is(Newline);
                     let lhs = enum_unwrap!(stack.pop(), Some:(ExprOrOp::Expr:(_)));
                     let sig = self
                         .convert_rhs_to_lambda_sig(lhs)
                         .map_err(|_| self.stack_dec())?;
                     self.counter.inc();
-                    let block = self.try_reduce_block().map_err(|_| self.stack_dec())?;
+                    let block = if is_multiline_block {
+                        self.try_reduce_block().map_err(|_| self.stack_dec())?
+                    } else {
+                        // precedence: `->` > `,`
+                        let expr = self
+                            .try_reduce_expr(false, false, false, false)
+                            .map_err(|_| self.stack_dec())?;
+                        Block::new(vec![expr])
+                    };
                     stack.push(ExprOrOp::Expr(Expr::Lambda(Lambda::new(
                         sig,
                         op,
@@ -1206,12 +1224,20 @@ impl Parser {
             match self.peek() {
                 Some(op) if op.category_is(TC::LambdaOp) => {
                     let op = self.lpop();
+                    let is_multiline_block = self.cur_is(Newline);
                     let lhs = enum_unwrap!(stack.pop(), Some:(ExprOrOp::Expr:(_)));
                     let sig = self
                         .convert_rhs_to_lambda_sig(lhs)
                         .map_err(|_| self.stack_dec())?;
                     self.counter.inc();
-                    let block = self.try_reduce_block().map_err(|_| self.stack_dec())?;
+                    let block = if is_multiline_block {
+                        self.try_reduce_block().map_err(|_| self.stack_dec())?
+                    } else {
+                        let expr = self
+                            .try_reduce_expr(false, false, false, false)
+                            .map_err(|_| self.stack_dec())?;
+                        Block::new(vec![expr])
+                    };
                     stack.push(ExprOrOp::Expr(Expr::Lambda(Lambda::new(
                         sig,
                         op,
diff --git a/doc/EN/syntax/00_basic.md b/doc/EN/syntax/00_basic.md
index f55f6d1d..fd49a2b7 100644
--- a/doc/EN/syntax/00_basic.md
+++ b/doc/EN/syntax/00_basic.md
@@ -25,7 +25,7 @@ This is almost identical to Python and other languages in the same family. The m
 In Erg, parentheses `()` can be omitted unless there is some confusion in interpretation.
 The omission of parentheses is similar to Ruby, but it is not possible to omit parentheses that can be interpreted in more than one way.
 
-```python
+```python,checker_ignore
 print! "Hello, World!" # OK
 print! "Hello,", "World!" # OK
 print!() # OK
@@ -81,7 +81,7 @@ The code after `#` is ignored as a comment. Use this to explain the intent of th
 # `#` and after are ignored until a new line is inserted
 #[
 Multi-line comment
-Treated as a comment all the way up to the corresponding `]#`
+Everything from `#[` to `]#` is a comment.
 ]#
 ```
 
@@ -93,6 +93,7 @@ Erg scripts are basically evaluated from left to right, top to bottom.
 
 ```python
 n = 1 # assignment expression
+f x, y = x + y # function definition
 f(1, 2) # function-call expression
 1 + 1 # operator-call expression
 f(1, 2); 1 + 1
diff --git a/doc/EN/syntax/02_name.md b/doc/EN/syntax/02_name.md
index 0840e981..ffaa5081 100644
--- a/doc/EN/syntax/02_name.md
+++ b/doc/EN/syntax/02_name.md
@@ -21,9 +21,12 @@ n: Nat = 1
 
 Note that, unlike other languages, multiple assignments are not allowed.
 
-```python
+```python,compile_fail
 # NG
 l1 = l2 = [1, 2, 3] # SyntaxError: multiple assignment not allowed
+```
+
+```python
 # OK
 l1 = [1, 2, 3]
 l2 = l1.clone()
@@ -51,7 +54,7 @@ assert x == 0
 
 The following may seem possible at first glance, but it is still not possible. This is a design decision, not a technical constraint.
 
-```python
+```python,compile_fail
 x = 0
 if x.is_zero(), do:
     x = x + 1 # NameError: cannot define variables refer to variables with the same name
@@ -64,7 +67,7 @@ assert x == 0
 Constants are also a type of algebra. If you start an identifier with a capital letter, it is treated as a constant. They are called constants because once defined, they do not change.
 The `N` part is called the constant name (or identifier). Otherwise, it is the same as a variable.
 
-```python
+```python,compile_fail
 N = 0
 if True, do:
     N = 1 # AssignError: constants cannot be shadowed
@@ -95,8 +98,11 @@ The above code prints `π` when `x` is `3.141592653589793`. If `x` is changed to
 Some objects cannot be bound as constants. Mutable objects, for example. Mutable objects are objects whose states can be changed, as described in detail later.
 This is because of the rule that only constant expressions can be assigned to constants. Constant expressions are also discussed later.
 
-```python
+```python,compile_fail
 X = 1 # OK
+```
+
+```python
 X = !1 # TypeError: cannot define Int! object as a constant
 ```
 
@@ -104,7 +110,7 @@ X = !1 # TypeError: cannot define Int! object as a constant
 
 You can delete an variable by using the `Del` function. All other variables that depend on the variable (that is, that refer directly to the value of the variable) are also removed.
 
-```python
+```python,checker_ignore
 x = 1
 y = 2
 Z = 3
@@ -130,8 +136,8 @@ Note that `x == a` is not necessarily true when `x = a`. An example is `Float.Na
 
 ```python
 x = Float.NaN
-assert x ! = NaN
-assert x ! = x
+assert x != NaN
+assert x != x
 ```
 
 There are other objects for which no equivalence relation is defined in the first place.
diff --git a/doc/EN/syntax/03_declaration.md b/doc/EN/syntax/03_declaration.md
index 1548c120..9204b114 100644
--- a/doc/EN/syntax/03_declaration.md
+++ b/doc/EN/syntax/03_declaration.md
@@ -26,20 +26,21 @@ i: Nat # this will not pass (-1 is not an element of Nat)
 
 Functions can be declared in 2 different ways.
 
-```python
+```python,checker_ignore
 f: (x: Int, y: Int) -> Int
 f: (Int, Int) -> Int
 ```
 
 If you declare the argument names explicitly, a type error will result if the names are different at definition time. If you want to give the argument names arbitrary names, you can declare them in the second way. In that case, only the method name and its type will be seen by type checking.
 
-```python
+```python,compile_fail
 T = Trait {
     .f = (x: Int, y: Int): Int
 }
 
-C = Class(U, Impl := T)
-C.f(a: Int, b: Int): Int = ... # TypeError: `.f` must be type of `(x: Int, y: Int) -> Int`, not `(a: Int, b: Int) -> Int`
+C = Class()
+C|<: T|.
+    f(a: Int, b: Int): Int = ... # TypeError: `.f` must be type of `(x: Int, y: Int) -> Int`, not `(a: Int, b: Int) -> Int`
 ```
 
 <p align='center'>
diff --git a/doc/EN/syntax/04_function.md b/doc/EN/syntax/04_function.md
index a782b3a3..787502be 100644
--- a/doc/EN/syntax/04_function.md
+++ b/doc/EN/syntax/04_function.md
@@ -4,6 +4,9 @@ A function is a block that takes an "argument", processes it, and returns it as
 
 ```python
 add x, y = x + y
+```
+
+```python
 # or
 add(x, y) = x + y
 ```
@@ -23,11 +26,11 @@ add(1, 2)
 
 Functions are invoked like `f x, y, ...`, but if there are too many arguments for a single line, they can be applied using `:` (colon).
 
-```python
+```python,checker_ignore
 f some_long_name_variable_1 + some_long_name_variable_2, some_long_name_variable_3 * some_long_name_variable_4
 ```
 
-```python
+```python,checker_ignore
 f some_long_name_variable_1 + some_long_name_variable_2:
     some_long_name_variable_3 * some_long_name_variable_4
 ```
@@ -47,12 +50,14 @@ result = if Bool.sample!():
 After `:`, no code other than comments may be written, and must always be on a new line.
 Also, you cannot use `:` immediately after a function. Only `do` and `do!` can do this.
 
-```python
+```python,compile_fail
 # NG
 f:
     x
     y
+```
 
+```python,checker_ignore
 # Ok
 f(
     x,
@@ -71,7 +76,7 @@ f x, y, z, w, v, u: Int = ...
 
 The functions defined above have many arguments and are arranged in a confusing order. You should not create such a function, but you may encounter such code when using code written by others. Therefore, we use keyword arguments. If you use keyword arguments, the values are passed from the name to the correct argument, even if they are in the wrong order.
 
-```python
+```python,checker_ignore
 f u := 6, v := 5, w:= 4, x := 1, y := 2, z := 3
 ```
 
@@ -106,13 +111,13 @@ f [x, y] := [1, 2] = ...
 
 However, within the default arguments, it is not possible to call the procedures (described later) or assign mutable objects.
 
-```python
+```python,compile_fail
 f x := p! 1 = ... # NG
 ```
 
 Also, the argument just defined cannot be used as the value passed to the default argument.
 
-```python
+```python,compile_fail
 f x := 1, y := x = ... # NG
 ```
 
@@ -231,7 +236,9 @@ assert Add(1, 2) == 3
 Factorial 0 = 1
 Factorial(X: Nat): Nat = X * Factorial(X - 1)
 assert Factorial(10) == 3628800
+```
 
+```python,compile_fail
 math = import "math"
 Sin X = math.sin X # ConstantError: this function is not computable at compile time
 ```
@@ -247,7 +254,7 @@ Option: Type -> Type
 
 Erg does not define `==` for functions. This is because there is no structural equivalence algorithm for functions in general.
 
-```python
+```python,compile_fail
 f = x: Int -> (x + 1)**2
 g = x: Int -> x**2 + 2x + 1
 
@@ -257,7 +264,7 @@ assert f == g # TypeError: cannot compare functions
 Although `f` and `g` always return the same result, it is extremely difficult to make that determination. We have to teach algebra to the compiler.
 So Erg gives up on function comparisons entirely, and `(x -> x) == (x -> x)` also results in a compile error. This is a different specification from Python and should be noted.
 
-```python
+```python,checker_ignore
 # Python, weird example
 f = lambda x: x
 assert f == f
@@ -266,7 +273,7 @@ assert (lambda x: x) ! = (lambda x: x)
 
 ## Appendix2: ()-completion
 
-```python
+```python,checker_ignore
 f x: Object = ...
 # will be completed to
 f(x: Object) = ...
diff --git a/doc/EN/syntax/06_operator.md b/doc/EN/syntax/06_operator.md
index 7575f4e9..9ea64f12 100644
--- a/doc/EN/syntax/06_operator.md
+++ b/doc/EN/syntax/06_operator.md
@@ -5,14 +5,17 @@ Operators are symbols that represent operations. Operands are things to the (lef
 Operators are a kind of function, and thus are themselves first-class objects that can be bound to variables. When binding, it is necessary to enclose it with ``.
 For `+` (and `-`), there are both unary and binary operators, so `_+_`(binary operation)/`+_`(unary operation ) must be specified.
 
-```python
+```python,compile_fail
 add = `+` # SyntaxError: specify `_+_` or `+_`
-add=`_+_`
-assert f(1, 2) == 3
-assert f("a", "b") == "ab"
+```
 
-g = `*` # OK, this is binary only
-assert g(1, 2) == 2
+```python
+add = `_+_`
+assert add(1, 2) == 3
+assert add("a", "b") == "ab"
+
+mul = `*` # OK, this is binary only
+assert mul(1, 2) == 2
 ```
 
 Some fundamental operators, called special forms, cannot be bound.
diff --git a/doc/EN/syntax/07_side_effect.md b/doc/EN/syntax/07_side_effect.md
index 895e6921..72c214b2 100644
--- a/doc/EN/syntax/07_side_effect.md
+++ b/doc/EN/syntax/07_side_effect.md
@@ -40,7 +40,7 @@ Only one procedural methods can have a mutable reference at any given time. In a
 
 Note, however, that it is possible to create (immutable/mutable) references from mutable references. This allows recursion and `print!` of `self` in procedural methods.
 
-```python
+```python,checker_ignore
 T -> T # OK (move)
 T -> Ref T # OK (move)
 T => Ref! T # OK (only once)
@@ -70,7 +70,7 @@ assert nan(1) ! = nan(1)
 
 There are also objects, such as classes, for which equivalence determination itself is not possible.
 
-```python
+```python,checker_ignore
 T = Structural {i = Int}
 U = Structural {i = Int}
 assert T == U
diff --git a/doc/EN/syntax/11_tuple.md b/doc/EN/syntax/11_tuple.md
index b20b67eb..6820f539 100644
--- a/doc/EN/syntax/11_tuple.md
+++ b/doc/EN/syntax/11_tuple.md
@@ -27,9 +27,12 @@ i, b, s = t
 
 Tuples can hold objects of different types, so they cannot be iterated like arrays.
 
-```python
+```python,compile_fail
 t: ({1}, {2}, {3}) = (1, 2, 3)
 (1, 2, 3).iter().map(x -> x + 1) # TypeError: type ({1}, {2}, {3}) has no method `.iter()`
+```
+
+```python
 # If all types are the same, they can be represented by `(T; n)` like arrays, but this still does not allow iteration
 t: (Int; 3) = (1, 2, 3)
 assert (Int; 3) == (Int, Int, Int)
diff --git a/doc/EN/syntax/13_record.md b/doc/EN/syntax/13_record.md
index fd87649c..1e0c304e 100644
--- a/doc/EN/syntax/13_record.md
+++ b/doc/EN/syntax/13_record.md
@@ -20,11 +20,11 @@ So how should we use dictionaries and records?
 In general, we recommend using records. Records have the advantages of being checked at compile-time for the existence of elements and of being able to specify __visibility_.
 Specifying visibility is equivalent to specifying public/private in Java and other languages. For details, see [visibility](./19_visibility.md) for details.
 
-```python
+```python,compile_fail
 a = {x = 1; .y = x + 1}
+assert a.y == 2
 a.x # AttributeError: x is private
 # Hint: declare as `.x`.
-assert a.y == 2
 ```
 
 The above example may seem strange to someone familiar with JavaScript, but simply declaring `x` makes it inaccessible from the outside. `. `. `.
@@ -33,7 +33,7 @@ You can also explicitly specify the type of an attribute.
 
 ```python
 anonymous = {
-    .name: Option! Str = !
+    .name: Option! Str = !""
     .age = 20
 }
 anonymous.name.set! "John"
@@ -169,28 +169,28 @@ y =
 A bare record (a record generated by a record literal) must be defined directly in the instance if you try to implement a method on its own.
 This is inefficient, and as the number of attributes increases, error messages and the like become difficult to see and use.
 
-```python
+```python,compile_fail
 john = {
     name = "John Smith"
     age = !20
     .greet! ref self = print! "Hello, my name is \{self::name} and I am \{self::age} years old."
     .inc_age! ref! self = self::age.update! x -> x + 1
 }
-john + 1
+print! john + 1
 # TypeError: + is not implemented for {name = Str; age = Int; .greet! = Ref(Self). () => None; inc_age! = Ref! () => None}, Int
 ```
 
 So, in such a case, you can inherit a record class. Such a class is called a data class.
 This is described in [class](./type/04_class.md).
 
-```python
+```python,checker_ignore
 Person = Inherit {name = Str; age = Nat}
 Person.
     greet! ref self = print! "Hello, my name is \{self::name} and I am \{self::age} years old."
     inc_age! ref! self = self::age.update! x -> x + 1
 
 john = Person.new {name = "John Smith"; age = 20}
-john + 1
+print! john + 1
 # TypeError: + is not implemented for Person, Int
 ```
 
diff --git a/doc/EN/syntax/15_type.md b/doc/EN/syntax/15_type.md
index 8430dc74..97b8bad7 100644
--- 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>
\ No newline at end of file
+</p>
diff --git a/doc/EN/syntax/16_iterator.md b/doc/EN/syntax/16_iterator.md
index 2057ce78..e22d0331 100644
--- a/doc/EN/syntax/16_iterator.md
+++ b/doc/EN/syntax/16_iterator.md
@@ -8,7 +8,7 @@ for! 0..9, i =>
 ```
 
 This code prints the numbers 0 through 9.
-Each number (=Int object) is assigned to `i` and the following operation (=`print! i``) is executed. This kind of repetitive execution is called __iteration__.
+Each number (=Int object) is assigned to `i` and the following operation (=`print! i`) is executed. This kind of repetitive execution is called __iteration__.
 
 Now let's look at the type signature of the `for!` procedure.
 
diff --git a/doc/EN/syntax/18_ownership.md b/doc/EN/syntax/18_ownership.md
index 81ca9e4f..59ee6b79 100644
--- a/doc/EN/syntax/18_ownership.md
+++ b/doc/EN/syntax/18_ownership.md
@@ -57,9 +57,7 @@ sum|T <: Add + HasUnit| i: Iterator T = ...
 
 x = [1, 2, 3].into [Int; !3]
 x.push!(4)
-i = x.iter() # TypeError: [Int; !4] has no method `iter`
-y = x.freeze()
-i = y.iter()
+i = x.iter()
 assert sum(i) == 10
 y # y can still be touched
 ```
@@ -107,4 +105,4 @@ Erg is designed to prevent unintentional memory leaks, and will issue an error i
 
 <p align='center'>
     <a href='./17_mutability.md'>Previous</a> | <a href='./19_visibility.md'>Next</a>
-</p>
\ No newline at end of file
+</p>
diff --git a/doc/EN/syntax/19_visibility.md b/doc/EN/syntax/19_visibility.md
index 414f6f66..64d0911c 100644
--- a/doc/EN/syntax/19_visibility.md
+++ b/doc/EN/syntax/19_visibility.md
@@ -23,7 +23,7 @@ Public variables are defined with `.`.
 .x = "this is a visible variable"
 ```
 
-```python
+```python,checker_ignore
 # bar.er
 foo = import "foo"
 assert foo.x == "this is a visible variable"
@@ -96,13 +96,15 @@ A class defined in one module can actually define methods from an external modul
 
 ```python
 # bar.er
-{Foo; ...} = import "foo"
+{Foo;} = import "foo"
 
 Foo::
     private self = pass
 Foo.
     public self = self::private()
+```
 
+```python,compile_fail
 .f() =
     foo = Foo.new()
     foo.public()
@@ -113,9 +115,9 @@ 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.
 
-```python
+```python,compile_fail
 # baz.er
-{Foo; ...} = import "foo"
+{Foo;} = import "foo"
 
 foo = Foo.new()
 foo.public() # AttributeError: 'Foo' has no attribute 'public' ('public' is defined in module 'bar')
@@ -126,7 +128,7 @@ This is to avoid confusion about methods being found or not found depending on t
 
 ```python,compile_fail
 # bar.er
-{.Foo; ...} = import "foo"
+{.Foo;} = import "foo"
 
 .Foo::
     private self = pass # Error
@@ -138,7 +140,7 @@ If you want to do something like this, define a [patch](./type/07_patch.md).
 
 ```python
 # bar.er
-{Foo; ...} = import "foo"
+{Foo;} = import "foo"
 
 FooImpl = Patch Foo
 FooImpl :=:
@@ -149,8 +151,8 @@ Foo Impl.
 
 ```python
 # baz.er
-{Foo; ...} = import "foo"
-{FooImpl; ...} = import "bar"
+{Foo;} = import "foo"
+{FooImpl;} = import "bar"
 
 foo = Foo.new()
 foo.public()
@@ -161,7 +163,7 @@ foo.public()
 Variable visibility is not limited to complete public/private.
 You can also publish with restrictions.
 
-```python
+```python,checker_ignore
 # foo.er
 .record = {
     .a = {
@@ -179,7 +181,7 @@ _ = .record.a.y # OK
 _ = .record.a.z # OK
 ```
 
-```python
+```python,checker_ignore
 foo = import "foo"
 _ = foo.record.a.x # VisibilityError
 _ = foo.record.a.y # VisibilityError
@@ -188,4 +190,4 @@ _ = foo.record.a.z # OK
 
 <p align='center'>
     <a href='./18_ownership.md'>Previous</a> | <a href='./20_naming_rule.md'>Next</a>
-</p>
\ No newline at end of file
+</p>
diff --git a/doc/EN/syntax/21_lambda.md b/doc/EN/syntax/21_lambda.md
index 136a4d36..47067671 100644
--- a/doc/EN/syntax/21_lambda.md
+++ b/doc/EN/syntax/21_lambda.md
@@ -92,4 +92,4 @@ id = |T| x: T -> x
 
 <p align='center'>
     <a href='./20_naming_rule.md'>Previous</a> | <a href='./22_subroutine.md'>Next</a>
-</p>
\ No newline at end of file
+</p>
diff --git a/doc/EN/syntax/22_subroutine.md b/doc/EN/syntax/22_subroutine.md
index b671e828..8e55a371 100644
--- a/doc/EN/syntax/22_subroutine.md
+++ b/doc/EN/syntax/22_subroutine.md
@@ -2,14 +2,14 @@
 
 ## Func
 
-```python
+```python,checker_ignore
 some_func(x: T, y: U) -> V
 some_func: (T, U) -> V
 ```
 
 ## Proc
 
-```python
+```python,checker_ignore
 some_proc!(x: T, y: U) => V
 some_proc!: (T, U) => V
 ```
@@ -18,7 +18,7 @@ some_proc!: (T, U) => V
 
 The method type cannot be specified externally with ``Self``.
 
-```python
+```python,checker_ignore
 .some_method(self, x: T, y: U) => ()
 # Self.(T, U) => () takes ownership of self
 .some_method: (Ref(Self), T, U) => ()
@@ -28,13 +28,13 @@ The method type cannot be specified externally with ``Self``.
 
 In the following, assume that the type `T!` takes the type argument `N: Nat`. To specify it externally, use a type variable.
 
-```python
-T!: Nat -> Type
+```python,checker_ignore
+K!: Nat -> Type
 # ~> indicates the state of the type argument before and after application (in this case, self must be a variable reference)
-T!(N).some_method!: (Ref!(T! N ~> N+X), X: Nat) => ()
+K!(N).some_method!: (Ref!(K! N ~> N+X), X: Nat) => ()
 ```
 
-As a note, the type of `.some_method` is `|N, X: Nat| (Ref!(T N ~> N+X), {X}) => ()`.
+As a note, the type of `.some_method` is `|N, X: Nat| (Ref!(K! N ~> N+X), {X}) => ()`.
 For methods that do not have `ref!`, i.e., are deprived of ownership after application, the type argument transition (`~>`) cannot be used.
 
 If ownership is taken, it is as follows.
diff --git a/doc/EN/syntax/23_closure.md b/doc/EN/syntax/23_closure.md
index 6675ae9f..0725b0c2 100644
--- a/doc/EN/syntax/23_closure.md
+++ b/doc/EN/syntax/23_closure.md
@@ -60,7 +60,7 @@ assert sum == 45
 
 The equivalent program above can be written in Python as follows:
 
-```python
+```python,checker_ignore
 # Python
 sum = 0
 for i in range(1, 10):
@@ -93,4 +93,4 @@ Erg is designed to be a natural succinct description of programming with immutab
 
 <p align='center'>
     <a href='./22_subroutine.md'>Previous</a> | <a href='./24_module.md'>Next</a>
-</p>
\ No newline at end of file
+</p>
diff --git a/doc/EN/syntax/24_module.md b/doc/EN/syntax/24_module.md
index 44c9ff33..b4fb8ca4 100644
--- a/doc/EN/syntax/24_module.md
+++ b/doc/EN/syntax/24_module.md
@@ -12,7 +12,7 @@ Erg allows you to think of the file itself as a single record. This is called a
 foo = {.i = 1}
 ```
 
-```python: bar.er
+```python,checker_ignore
 # bar.er
 foo = import "foo"
 print! foo # <module 'foo'>
@@ -20,9 +20,11 @@ assert foo.i == 1
 ```
 
 Since module types are also record types, deconstruction assignment is possible.
+For modules, you can omit the trailing `...`.
 
 ```python
-{sin; cos; ...} = import "math"
+# same as {sin; cos; ...} = import "math"
+{sin; cos} = import "math"
 ```
 
 ## Module Visibility
@@ -94,7 +96,7 @@ print! foo.f 1
 However, variables created by procedure calls cannot be defined in circular reference modules.
 This is because Erg rearranges the order of definitions according to dependencies.
 
-```python
+```python,compile_fail
 # foo.er
 bar = import "bar"
 
diff --git a/doc/EN/syntax/26_pattern_matching.md b/doc/EN/syntax/26_pattern_matching.md
index 3cf74040..8f854b71 100644
--- a/doc/EN/syntax/26_pattern_matching.md
+++ b/doc/EN/syntax/26_pattern_matching.md
@@ -64,7 +64,7 @@ name = match num:
 
 ### Refinement pattern
 
-```python
+```python,checker_ignore
 # these two are the same
 Array(T, N: {N | N >= 3})
 Array(T, N | N >= 3)
diff --git a/doc/EN/syntax/28_spread_syntax.md b/doc/EN/syntax/28_spread_syntax.md
index c2a5ca4b..c67a1680 100644
--- a/doc/EN/syntax/28_spread_syntax.md
+++ b/doc/EN/syntax/28_spread_syntax.md
@@ -38,4 +38,4 @@ assert x == 1 and y == 2
 
 <p align='center'>
     <a href='./27_comprehension.md'>Previous</a> | <a href='./29_decorator.md'>Next</a>
-</p>
\ No newline at end of file
+</p>
diff --git a/doc/EN/syntax/29_decorator.md b/doc/EN/syntax/29_decorator.md
index 7b1992a0..4f134382 100644
--- a/doc/EN/syntax/29_decorator.md
+++ b/doc/EN/syntax/29_decorator.md
@@ -5,7 +5,7 @@ The syntax of the decorator is as follows.
 
 ```python
 @deco
-X=...
+X = ...
 ```
 
 You can have multiple decorators as long as they don't conflict.
@@ -13,7 +13,7 @@ You can have multiple decorators as long as they don't conflict.
 A decorator is not a special object, it's just a one-argument function. The decorator is equivalent to the following pseudocode.
 
 ```python
-X=...
+X = ...
 X = deco(X)
 ```
 
@@ -100,7 +100,7 @@ Internally it's just attached using the trait's `.attach` method. Conflicts can
 
 ```python
 @Attach X
-T = Trait...
+T = Trait ...
 assert X in T. attaches
 U = T.detach(X).attach(Y)
 assert X not in U. attaches
@@ -117,4 +117,4 @@ Indicates that this is a test subroutine. Test subroutines are run with the `erg
 
 <p align='center'>
     <a href='./28_spread_syntax.md'>Previous</a> | <a href='./30_error_handling.md'>Next</a>
-</p>
\ No newline at end of file
+</p>
diff --git a/doc/EN/syntax/30_error_handling.md b/doc/EN/syntax/30_error_handling.md
index c52d5cbf..333b464f 100644
--- a/doc/EN/syntax/30_error_handling.md
+++ b/doc/EN/syntax/30_error_handling.md
@@ -18,7 +18,7 @@ Specify `Error` in `pyimport` `exception_type` (`exception_type: {Error, Panic}`
 The `Result` type represents values ​​that may be errors. Error handling with `Result` is superior to the exception mechanism in several ways.
 First of all, it's obvious from the type definition that the subroutine might throw an error, and it's also obvious when you actually use it.
 
-```python
+```python,checker_ignore
 # Python
 try:
     x = foo().bar()
@@ -50,7 +50,7 @@ The benefits of using the `Result` type don't stop there. The `Result` type is a
 
 Since the `Error`/`Result` type alone does not cause side effects, unlike exceptions, it cannot have information such as the sending location (Context), but if you use the `.context` method, you can put information in the `Error` object. can be added. The `.context` method is a type of method that consumes the `Error` object itself and creates a new `Error` object. They are chainable and can hold multiple contexts.
 
-```python
+```python,chekcer_ignore
 f() =
     todo() \
         .context "to be implemented in ver 1.2" \
@@ -71,7 +71,7 @@ Therefore, in Erg, the `Error` object has an attribute called `.stack`, and repr
 `.stack` is an array of caller objects. Each time an Error object is `returned` (including by `?`) it pushes its calling subroutine onto the `.stack`.
 And if it is `?`ed or `.unwrap`ed in a context where `return` is not possible, it will panic with a traceback.
 
-```python
+```python,checker_ignore
 f x =
     ...
     y = foo.try_some(x)?
@@ -100,10 +100,10 @@ An unrecoverable error is an error caused by an external factor such as a softwa
 
 Panic is done with the `panic` function.
 
-```python
+```python,checker_ignore
 panic "something went wrong!"
 ```
 
 <p align='center'>
     <a href='./29_decorator.md'>Previous</a> | <a href='./31_pipeline.md'>Next</a>
-</p>
\ No newline at end of file
+</p>
diff --git a/doc/EN/syntax/32_integration_with_Python.md b/doc/EN/syntax/32_integration_with_Python.md
index 7068e2f0..3f75149e 100644
--- a/doc/EN/syntax/32_integration_with_Python.md
+++ b/doc/EN/syntax/32_integration_with_Python.md
@@ -15,7 +15,7 @@ private = "this is a private variable"
 erg --compile foo.er
 ```
 
-```python
+```python,checker_ignore
 import foo
 
 print(foo.public)
diff --git a/doc/EN/syntax/33_package_system.md b/doc/EN/syntax/33_package_system.md
index 930a9de5..d87b9a04 100644
--- a/doc/EN/syntax/33_package_system.md
+++ b/doc/EN/syntax/33_package_system.md
@@ -71,7 +71,7 @@ Also, modules that are not reimported in `__init__.er` are private modules and c
 .qux = import "qux" # this is public
 ```
 
-```python
+```python,checker_ignore
 # foo.er
 bar = import "bar"
 bar.qux
diff --git a/doc/EN/syntax/container_ownership.md b/doc/EN/syntax/container_ownership.md
index 7e5b813c..5e9e401d 100644
--- a/doc/EN/syntax/container_ownership.md
+++ b/doc/EN/syntax/container_ownership.md
@@ -15,13 +15,16 @@ It is also not possible to reproduce the behavior of `[]` in a method.
 
 ```python
 C = Class {i = Int!}
-C. get(ref self) =
-    self::i # TypeError: `self::i` is `Int!` (require ownership) but `get` doesn't own `self`
 C.steal(self) =
     self::i
-# NG
-C.new({i = 1}).steal().inc!() # OwnershipWarning: `C.new({i = 1}).steal()` is not owned by anyone
-# hint: assign to a variable or use `uwn_do!`
+```
+
+```python,compile_fail
+C.get(ref self) =
+    self::i # TypeError: `self::i` is `Int!` (require ownership) but `get` doesn't own `self`
+```
+
+```python
 # OK (assigning)
 c = C.new({i = 1})
 i = c.steal()
@@ -31,12 +34,18 @@ assert i == 2
 own_do! C.new({i = 1}).steal(), i => i.inc!()
 ```
 
+```python
+# NG
+C.new({i = 1}).steal().inc!() # OwnershipWarning: `C.new({i = 1}).steal()` is not owned by anyone
+# hint: assign to a variable or use `uwn_do!`
+```
+
 Also, `[]` can be disowned, but the element is not shifted.
 
-```python
+```python,compile_fail
 a = [!1, !2]
 i = a[0]
 i.inc!()
 assert a[1] == 2
 a[0] # OwnershipError: `a[0]` is moved to `i`
-```
\ No newline at end of file
+```
diff --git a/doc/JA/syntax/24_module.md b/doc/JA/syntax/24_module.md
index 7aea2708..ef915c58 100644
--- a/doc/JA/syntax/24_module.md
+++ b/doc/JA/syntax/24_module.md
@@ -22,9 +22,11 @@ assert foo.i == 1
 ```
 
 モジュール型はレコード型でもあるので、分解代入が可能です。
+モジュールの場合は最後の`...`を省略できます。
 
 ```python
-{sin; cos; ...} = import "math"
+# same as {sin; cos; ...} = import "math"
+{sin; cos} = import "math"
 ```
 
 ## モジュールの可視性
diff --git a/examples/mut.er b/examples/mut.er
new file mode 100644
index 00000000..55468984
--- /dev/null
+++ b/examples/mut.er
@@ -0,0 +1,8 @@
+i = !1
+i.update! i -> i * 3
+assert i == 3
+
+i.inc!()
+assert i == 4
+i.dec!()
+assert i == 3
diff --git a/src/main.rs b/src/main.rs
index ce0139e7..446183b2 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -9,6 +9,7 @@ use std::thread;
 use erg_common::config::ErgConfig;
 use erg_common::traits::Runnable;
 
+use erg_parser::build_ast::ASTBuilder;
 use erg_parser::lex::LexerRunner;
 use erg_parser::ParserRunner;
 
@@ -29,6 +30,9 @@ fn run() {
         "parse" => {
             ParserRunner::run(cfg);
         }
+        "desugar" => {
+            ASTBuilder::run(cfg);
+        }
         "lower" => {
             ASTLowerer::run(cfg);
         }
diff --git a/tests/should_err/infer_union_array.er b/tests/should_err/infer_union_array.er
new file mode 100644
index 00000000..0cae4c02
--- /dev/null
+++ b/tests/should_err/infer_union_array.er
@@ -0,0 +1,6 @@
+f x: [{""}; _] = None
+
+arr = ["aaa"]
+for! arr, elem =>
+    a = ["", "aaa"] # [{"", "aaa"}; 2]
+    f a # ERR: type mismatched
diff --git a/tests/test.rs b/tests/test.rs
index c9a54447..e8479e3a 100644
--- a/tests/test.rs
+++ b/tests/test.rs
@@ -84,6 +84,11 @@ fn exec_infer_trait() -> Result<(), ()> {
     expect_success("tests/should_ok/infer_trait.er")
 }
 
+#[test]
+fn exec_mut() -> Result<(), ()> {
+    expect_success("examples/mut.er")
+}
+
 #[test]
 fn exec_patch() -> Result<(), ()> {
     expect_success("examples/patch.er")
@@ -149,6 +154,11 @@ fn exec_args() -> Result<(), ()> {
     expect_failure("tests/should_err/args.er", 16)
 }
 
+#[test]
+fn exec_infer_union_array() -> Result<(), ()> {
+    expect_failure("tests/should_err/infer_union_array.er", 1)
+}
+
 #[test]
 fn exec_invalid_param() -> Result<(), ()> {
     expect_failure("tests/should_err/invalid_param.er", 3)