Add no-check and expr for linting.

course4/course4_en.md

@@ -60,14 +60,14 @@ headingDivider: 1
 
 - Access to the fields of a structure: `<structure>.<field>`
 
-```moonbit
+```moonbit no-check
 let old_info: PersonalInfo = { name: "Moonbit", age: 1, }
 let a: Int = old_info.age // 1
 ```
 
 - To update the original structure, we can reuse the original part:
 
-```moonbit
+```moonbit no-check
 let new_info = { .. old_info, age: 2, }
 let other_info = { .. old_info, name: "Hello", }
 ```
@@ -81,7 +81,7 @@ let other_info = { .. old_info, name: "Hello", }
         - `f(g(b)) == b`
 - Example: `struct PersonalInfo { name: String; age: Int }` is **isomorphic** to `(String, Int)`
 
-```moonbit
+```moonbit no-check
 fn f(info: PersonalInfo) -> (String, Int) { (info.name, info.age) }
 fn g(pair: (String, Int)) -> PersonalInfo { { name: pair.0, age: pair.1, }}
 ```
@@ -92,7 +92,7 @@ fn g(pair: (String, Int)) -> PersonalInfo { { name: pair.0, age: pair.1, }}
 
 - Tuples are **structural**: as long as the structure is the same (field types correspond one by one), they are type compatible
 
-```moonbit
+```moonbit no-check
 fn accept(tuple: (Int, String)) -> Bool {
   true
 }
@@ -101,7 +101,7 @@ let accepted: Bool = accept((1, "Yes"))
 
 - Structures are **nominal**: only when the type names are the same are they type compatible
 
-```moonbit
+```moonbit no-check
 struct A { val : Int ; other: Int }
 struct B { val : Int ; other: Int }
 fn accept(a: A) -> Bool {
@@ -115,7 +115,7 @@ let accepted: Bool = accept(({other: 2, val: 1}: A))
 
 - We can use pattern matching to eliminate tuples and structures
 
-```moonbit
+```moonbit no-check
 fn head_opt(list: List[Int]) -> Option[Int] {
   match list {
     Nil => None
@@ -124,7 +124,7 @@ fn head_opt(list: List[Int]) -> Option[Int] {
 }
 ```
 
-```moonbit
+```moonbit no-check
 fn get_or_else(option_int: Option[Int], default: Int) -> Int {
   match option_int {
     None => default
@@ -137,7 +137,7 @@ fn get_or_else(option_int: Option[Int], default: Int) -> Int {
 
 - Match **values** (booleans, numbers, characters, strings) or **constructors**
 
-```moonbit
+```moonbit no-check
 fn is_zero(i: Int) -> Bool {
   match i {
     0 => true
@@ -149,7 +149,7 @@ fn is_zero(i: Int) -> Bool {
 
 - Constructors can be **nested patterns** or **identifiers** to bind corresponding structures
 
-```moonbit
+```moonbit no-check
 fn contains_zero(l: List[Int]) -> Bool {
   match l {
     Nil => false
@@ -163,7 +163,7 @@ fn contains_zero(l: List[Int]) -> Bool {
 
 - Pattern matching for tuples requires one-to-one correspondence
 
-```moonbit
+```moonbit no-check
 fn first(pair: (Int, Int)) -> Int {
   match pair {
     (first, second) => first
@@ -173,7 +173,7 @@ fn first(pair: (Int, Int)) -> Int {
 
 - Pattern matching for structures can match partial fields; you can use the original field name as the identifier
 
-```moonbit
+```moonbit no-check
 fn baby_name(info: PersonalInfo) -> Option[String] {
   match info {
     { age: 0, .. } => None
@@ -186,7 +186,7 @@ fn baby_name(info: PersonalInfo) -> Option[String] {
 
 Function `zip` combines two lists into a new list of pairs like a zipper. The length of the resulting list is the minimum of the lengths of the input lists.
 
-```moonbit
+```moonbit no-check
 fn zip(l1: List[Int], l2: List[Char]) -> List[(Int ,Char)] {
   match (l1, l2) {
     (Cons(hd, tl), Cons(hd2, tl2)) => Cons((hd, hd2), zip(tl, tl2))
@@ -201,7 +201,7 @@ fn zip(l1: List[Int], l2: List[Char]) -> List[(Int ,Char)] {
 
 Note that the order of pattern matching is from top to bottom
 
-```moonbit
+```moonbit no-check
 fn zip(l1: List[Int], l2: List[Char]) -> List[(Int ,Char)] {
   match (l1, l2) {
     _ => Nil
@@ -235,13 +235,13 @@ The value of the expression is bound to the identifier defined according to the
 
 To represent different cases of data structures, we use enumerated types
 
-```moonbit
+```moonbit no-check
 enum DaysOfWeek {
   Monday; Tuesday; Wednesday; Thursday; Friday; Saturday; Sunday
 }
 ```
 
-```moonbit
+```moonbit no-check
 enum Coin {
   Head
   Tail
@@ -250,21 +250,21 @@ enum Coin {
 
 # Definition and Construction of Enumerated Types
 
-```moonbit
+```moonbit no-check
 enum DaysOfWeek {
   Monday; Tuesday; Wednesday; Thursday; Friday; Saturday; Sunday
 }
 ```
 
 - Every variant is a contructor
-```moonbit
+```moonbit no-check
 let monday: DaysOfWeek = Monday
 let tuesday: DaysOfWeek = Tuesday 
 ```
 
 - Variant names can be ambiguous. We use `<type>::` to disambiguate
 
-```moonbit
+```moonbit no-check
 enum Repeat1 { A; B }
 enum Repeat2 { A; B }
 let x: Repeat1 = Repeat1::A  
@@ -274,15 +274,15 @@ let x: Repeat1 = Repeat1::A
 
 - Enumerated types can distinguish themselves from existing types and abstract better
 
-```moonbit
+```moonbit no-check
 fn tomorrow(today: Int) -> Int
 fn tomorrow(today: DaysOfWeek) -> DaysOfWeek
 let tuesday = 1 * 2 // Is this Tuesday?
 ``` 
 
 - Preventing the representation of irrational data
 
-```moonbit
+```moonbit no-check
 struct UserId { email: Option[String]; telephone: Option[Int] }
 enum UserId {
   Email(String)
@@ -294,14 +294,14 @@ enum UserId {
 
 - Carrying data in variants
 
-```moonbit
+```moonbit no-check
 enum Option[T] {
     Some(T)
     None
 }
 ```
 
-```moonbit
+```moonbit no-check
 enum ComputeResult {
     Success(Int)
     Overflow
@@ -327,13 +327,13 @@ We call tuples, structures, enumerated types, etc. algebraic data types, which h
 
 - $1 \times n = n$
     - For any type `T`, `(T, Unit)` is isomorphic to `T`
-    ```moonbit
+    ```moonbit no-check
     fn f[T](t: T) -> (T, Unit) { (t, ()) }
     fn g[T](pair: (T, Unit)) -> T { pair.0 }
     ```
 - $0 + n = n$
     - For any type `T`, `enum PlusZero[T] { CaseT(T); CaseZero(Nothing) }` is isomorphic to `T`
-    ```moonbit
+    ```moonbit no-check
     fn f[T](t: PlusZero) -> T {
       match t {
         CaseT(t) => t

course4/lecture4_en.md

@@ -8,7 +8,7 @@ First, review the fundamental data type in MoonBit introduced in course 2: Tuple
 
 A MoonBit tuple is a composite of data which have different types with a fixed length. In comparison, lists are collections of data which have the same type with arbitrary lengths. For example, the length of the list below is not fixed, but the values stored must all be of the character type. In the previous lesson, we didn't discuss why `Cons` is named `Cons`. It is an abbreviation for `Construct`.
 
-```moonbit
+```moonbit no-check
 Cons('H', Cons('i', Cons('!', Nil)))
 ```
 
@@ -32,9 +32,15 @@ The problem is that it is hard to understand the data represented by tuples. For
 
 Structures allow us to assign **names** to the data, both to the entire type and to each field individually. For instance:
 
-- `struct PersonalInfo { name: String; age: Int }`
-- `struct ContactInfo { name: String; telephone: Int }`
-- `struct AddressInfo { address: String; postal: Int }`
+- ```moonbit
+  struct PersonalInfo { name: String; age: Int }
+  ```
+- ```moonbit
+  struct ContactInfo { name: String; telephone: Int }
+  ```
+- ```moonbit
+  struct AddressInfo { address: String; postal: Int }
+  ```
 
 We can clearly understand the information about the data and the meaning of each corresponding field by names.
 
@@ -44,7 +50,7 @@ Definitions of the values of a structure are enclosed in braces, with each field
 
 Accessing the fields of a structure is similar to tuples – by using the field name to retrieve the corresponding data, for example, `.age` to retrieve the field `age`. When creating a new structure based on an existing one, redeclaring each field can be tedious, especially if the original structure is large. For convenience, MoonBit also provides a feature to update only specific fields. We can simply indicate the base structure with `.. <original_structure>` before the definition of the structure values, and then only declare the fields that have been modified. See the example below.
 
-```moonbit
+```moonbit no-check
 let new_info = { .. old_info, age: 2, }
 let other_info = { .. old_info, name: "Hello", }
 ```
@@ -57,7 +63,7 @@ You may notice that tuples and structures seem quite similar. In fact, a structu
 
 For example, `PersonalInfo` and `(String, Int)` are isomorphic, as we can establish the following pair of mappings:
 
-```moonbit
+```moonbit expr
 fn f(info: PersonalInfo) -> (String, Int) { (info.name, info.age) }
 
 fn g(pair: (String, Int)) -> PersonalInfo { { name: pair.0, age: pair.1, }}
@@ -76,7 +82,7 @@ let accepted: Bool = accept((1, "Yes"))
 
 On the other hand, structures are *nominal*, meaning compatibility is based on the type name, and the internal order can be rearranged. In the first example, even though the structures are identical, the function cannot accept the structure because the type names are different. In the second example, the function can accept it because the types are the same even if the order of the fields is different.
 
-```moonbit
+```moonbit no-check
 struct A { val : Int ; other: Int }
 struct B { val : Int ; other: Int }
 fn accept(a: A) -> Bool {
@@ -171,7 +177,7 @@ We define our function with pattern matching. Here, we match a pairs by construc
 
 Lastly, pattern matching is not limited to `match`; it can also be used in data binding. In local definitions, we can use pattern matching expressions to bind corresponding substructures to identifiers. It's essential to note that if the match fails, the program will encounter a runtime error and terminate.
 
-```moonbit
+```moonbit no-check
 let ok_one = Result::Ok(1);
 let Result::Ok(one) = ok_one; 
 let Result::Err(e) = ok_one; // Runtime error
@@ -198,15 +204,15 @@ enum Coin {
 
 The construction of an enumerated type is as follows:
 
-```moonbit
+```moonbit no-check
 enum <type_name> { <variant>; }
 ```
 
 Here, each possible variant is a constructor. For instance, `let monday = Monday`, where `Monday` defines the day of the week as Monday. Different enumerated types may cause conflicts because they might use the same names for some cases. In such cases, we distinguish them by adding `<type>::` in front of the constructor, such as `DaysOfWeek::Monday`.
 
 Now we need to ask, why do we need enumerated types? Why not just use numbers from one to seven to represent Monday to Sunday? Let's compare the following two functions. 
 
-```moonbit
+```moonbit no-check
 fn tomorrow(today: Int) -> Int
 fn tomorrow(today: DaysOfWeek) -> DaysOfWeek
 let tuesday = 1 * 2 // Is this Tuesday?
@@ -247,24 +253,26 @@ Here, **Zero** is a type that corresponds to an **empty type**. We can define an
 
 Let's verify the properties mentioned earlier: any number multiplied by 1 equals itself, and any number plus 0 equals itself.
 
-```moonbit
+```moonbit no-check
 fn f[T](t: T) -> (T, Unit) { (t, ()) }
 fn g[T](pair: (T, Unit)) -> T { pair.0 }
 ```
 
 In this context, a type `T` multiplied by 1 implies that `(T, Unit)` is isomorphic to `T`. We can establish a set of mappings: it's straightforward to go from `T` to `(T, Unit)` by simply adding the zero-tuple. Conversely, going from `(T, Unit)` to `T` involves ignoring the zero-tuple. You can intuitively find that they are isomorphic. 
 
 ```moonbit
+enum Nothing {}
+
 enum PlusZero[T] { CaseT(T); CaseZero(Nothing) }
 
-fn f[T](t: PlusZero) -> T {
+fn f[T](t: PlusZero[T]) -> T {
   match t {
     CaseT(t) => t
     CaseZero(_) => abort("Impossible case, no such value.")
   }
 }
 
-fn g[T](t: T) -> PlusZero { CaseT(t) }
+fn g[T](t: T) -> PlusZero[T] { CaseT(t) }
 ```
 
 The property of any type plus zero equals itself means that, for any type, we define an enumerated type `PlusZero`. One case contains a value of type `T`, and the other case contains a value of type `Nothing`. This type is isomorphic to `T`, and we can construct a set of mappings. Starting with `PlusZero`, we use pattern matching to discuss the cases. If the included value is of type `T`, we map it directly to `T`. If the type is `Nothing`, this case will never happen because there are no values of type `Nothing`, so we use `abort` to handle, indicating that the program will terminate. Conversely, we only need to wrap `T` with `CaseT`. It's essential to emphasize that this introduction is quite basic, providing an intuitive feel. Explore further if you are interested.
@@ -277,7 +285,7 @@ enum Coins { Head; Tail }
 
 $\texttt{Coins} = 1 + 1 = 2$
 
-```moonbit
+```moonbit no-check
 enum DaysOfWeek { Monday; Tuesday; ...; }
 ```