update math eqs

HOME_EXAM.md

@@ -199,8 +199,9 @@ An expression can be either a
 - f, function
 
 Function sequence
-
-$<f, σ>⇓σ'$
+```math
+<f, σ>⇓σ'
+```
 
 ```rust
 fn main() {
@@ -210,8 +211,9 @@ fn main() {
 The function call moves the current state, $σ$ to the new derived state $σ'$ in the function, test()'s context. A function can evaluate void (none), i32 and bool.
 
 Command sequence
-
-$\frac{<c1,σ> ⇓ σ' <c2,σ'> ⇓ σ''}{<c1;c2,σ> ⇓ σ''}$
+```math
+\frac{<c1,σ> ⇓ σ' <c2,σ'> ⇓ σ''}{<c1;c2,σ> ⇓ σ''}
+```
 
 ```rust
 let x : i32 = 2;
@@ -220,8 +222,9 @@ test();
 A sequence is a composition of commands where the first command is first executed then the second command. Otherwise the intermediate step, $σ'$ would be lost.
 
 Operands for lhs, rhs arithmetic expressions
-
-$\frac{<e1,σ> ⇓ n1 <e2, σ> ⇓ n2}{<e1 + e2, σ> ⇓ n1 \text{ } plus \text{ } n2}$
+```math
+\frac{<e1,σ> ⇓ n1 <e2, σ> ⇓ n2}{<e1 + e2, σ> ⇓ n1 \text{ } plus \text{ } n2}
+```
 
 plus is addition as implemented in the computer. Other arithmetic operands imlemented are
 - -, minus
@@ -238,8 +241,9 @@ plus is addition as implemented in the computer. Other arithmetic operands imlem
 ```
 
 Operands for lhs, rhs boolean expressions
-
-$\frac{<e1,σ> ⇓ b1 <e2, σ> ⇓ b2}{<e1 == e2, σ> ⇓ b1 \text{ } equal \text{ } b2}$
+```math
+\frac{<e1,σ> ⇓ b1 <e2, σ> ⇓ b2}{<e1 == e2, σ> ⇓ b1 \text{ } equal \text{ } b2}
+```
 
 how equal is evaluated is up to the computer. Other boolean operands implemented are
 
@@ -254,24 +258,29 @@ how equal is evaluated is up to the computer. Other boolean operands implemented
 
 
 If true
-
-$\frac{<b, σ> ⇓ true <c1, σ> ⇓ σ'}{<if \text{ } b \text{ } then \text{ } c1> ⇓ σ}$
+```math
+\frac{<b, σ> ⇓ true <c1, σ> ⇓ σ'}{<if \text{ } b \text{ } then \text{ } c1> ⇓ σ}
+```
 
 then the state, $σ$ will change immediately to $σ'$.
 
 If false
-
-$\frac{<b, σ> ⇓ false <c1, σ> ⇓ σ''}{<if \text{ } b \text{ } then \text{ } c1> ⇓ σ}$
+```math
+\frac{<b, σ> ⇓ false <c1, σ> ⇓ σ''}{<if \text{ } b \text{ } then \text{ } c1> ⇓ σ}
+```
 
 the state, $σ'$ will be changed at the second command to $σ''$.
 
 While false
-
-$\frac{<b,σ> ⇓ false}{<while \text{ } b \text{ } do \text{ } c,σ> ⇓ σ}$
+```math
+\frac{<b,σ> ⇓ false}{<while \text{ } b \text{ } do \text{ } c,σ> ⇓ σ}
+```
 
 While true
+```math
+\frac{<b, σ> ⇓ true <c,σ> ⇓ σ' <while \text{ } b \text{ } do \text{ } c, σ'> ⇓ σ''}{<while \text{ } b \text{ } do \text{ } c,σ> ⇓ σ''}
+```
 
-$\frac{<b, σ> ⇓ true <c,σ> ⇓ σ' <while \text{ } b \text{ } do \text{ } c, σ'> ⇓ σ''}{<while \text{ } b \text{ } do \text{ } c,σ> ⇓ σ''}$
 ```rust
 let a : i32 = 0;
 while a < 5 {
@@ -282,8 +291,9 @@ while a < 5 {
 then $σ'$ is the result of the current state, $σ$ and the last state $σ''$ is the result of $σ'$.
 
 Let assignment expression
-
-$\frac{<x, σ>⇓<let \text{ } x:=e, σ>⇓σ'}{<let \text{ } x := e, σ> ⇓ σ[x := e]}$
+```math
+\frac{<x, σ>⇓<let \text{ } x:=e, σ>⇓σ'}{<let \text{ } x := e, σ> ⇓ σ[x := e]}
+```
 ```rust
 let a : i32 = 1;
 let b : bool = true;
@@ -292,8 +302,9 @@ let c : i32 = test(); // c will be assigned whaterver test() returns
 For let commands,  if the variable is already declared the state $σ$ will be changed to the one of the second command, state $σ'$, the variable will be lost. Otherwise the variable will be assigned to the state, $σ$.
 
 Assignment expression
-
-$\frac{}{<x := e, σ> ⇓ σ[x := e]}$
+```math
+\frac{}{<x := e, σ> ⇓ σ[x := e]}
+```
 
 ```rust
 x = 1;
@@ -307,8 +318,9 @@ For assignment, when the variable is assigned to a number, boolean or function t
 
 
 Return
-
-$\frac{<f, σ>⇓σ}{<return : e, σ> ⇓ σ[return : e]}$
+```math
+\frac{<f, σ>⇓σ}{<return : e, σ> ⇓ σ[return : e]}
+```
 
 ```rust
 fn main() -> i32 {
@@ -351,15 +363,17 @@ Types are now defined as
 
 
 Command sequence
-
-$\frac{<c1,σ> ⇓ σ' <c2,σ'> ⇓ σ''}{<c1;c2,σ> ⇓ σ''}$
+```math
+\frac{<c1,σ> ⇓ σ' <c2,σ'> ⇓ σ''}{<c1;c2,σ> ⇓ σ''}
+```
 
 as described in the SOS rules of the interpreter.
 
 
 Operands for i32 types
-
-$\frac{<e1,σ> ⇓ i32 <e2, σ> ⇓ i32}{<e1 + e2, σ> ⇓ i32}$
+```math
+\frac{<e1,σ> ⇓ i32 <e2, σ> ⇓ i32}{<e1 + e2, σ> ⇓ i32}
+```
 
 To operate these operands the expression need to evaluate to i32. Other arithmetic operands imlemented are
 - -, minus
@@ -376,8 +390,9 @@ To operate these operands the expression need to evaluate to i32. Other arithmet
 ```
 
 Operands for boolean types
-
-$\frac{<e1,σ> ⇓ bool <e2, σ> ⇓ bool}{<e1 == e2, σ> ⇓ bool}$
+```math
+\frac{<e1,σ> ⇓ bool <e2, σ> ⇓ bool}{<e1 == e2, σ> ⇓ bool}
+```
 
 To operate these operands the expression need to evaluate to boolean. Other boolean operands implemented are
 
@@ -392,8 +407,9 @@ true || false;
 ```
 
 If true/false
-
-$\frac{<e, σ> ⇓ bool <c1, σ> ⇓ σ'}{<if \text{ } bool \text{ } then \text{ } c1> ⇓ σ}$
+```math
+\frac{<e, σ> ⇓ bool <c1, σ> ⇓ σ'}{<if \text{ } bool \text{ } then \text{ } c1> ⇓ σ}
+```
 
 ```rust
 if false {
@@ -402,22 +418,25 @@ if false {
 ```
 
 While true/false
-
-$\frac{<e, σ> ⇓ bool <c,σ> ⇓ σ' <while \text{ } bool \text{ } do \text{ } c, σ'> ⇓ σ''}{<while \text{ } bool \text{ } do \text{ } c,σ> ⇓ σ''}$
+```math
+\frac{<e, σ> ⇓ bool <c,σ> ⇓ σ' <while \text{ } bool \text{ } do \text{ } c, σ'> ⇓ σ''}{<while \text{ } bool \text{ } do \text{ } c,σ> ⇓ σ''}
+```
 
 For both if and while commands their block/scope are evluated as long as their condition is evaluted to the type boolean. This differ from the interpreter which only executes the block/scope if the condition is true.
 
 
 Let assignment i32 expression
-
-$\frac{<x, σ>⇓i32<let \text{ } x:=i32, σ>⇓σ'}{<let \text{ } x := i32, σ> ⇓ σ[x := i32]}$
+```math
+\frac{<x, σ>⇓i32<let \text{ } x:=i32, σ>⇓σ'}{<let \text{ } x := i32, σ> ⇓ σ[x := i32]}
+```
 ```rust
 let a : i32 = 1;
 let b : i32 = test(); // test() must return type i32 otherwise Error
 ```
 Let assignment bool expression
-
-$\frac{<x, σ>⇓bool<let \text{ } x:=bool, σ>⇓σ'}{<let \text{ } x := bool, σ> ⇓ σ[x := bool]}$
+```math
+\frac{<x, σ>⇓bool<let \text{ } x:=bool, σ>⇓σ'}{<let \text{ } x := bool, σ> ⇓ σ[x := bool]}
+```
 ```rust
 let a : bool = true;
 let b : bool = test(); // test() must return type bool otherwise Error
@@ -425,15 +444,17 @@ let b : bool = test(); // test() must return type bool otherwise Error
 As previously mentioned, let assignment are unique declerations. Thus, the same variable can not be declared twice in the same scope. Here, the given return type of the variable is checked with rhs evluated type.
 
 Assignment i32 expression
-
-$\frac{<x, σ> ⇓ i32<e, σ> i32}{<x := i32, σ> ⇓ σ[x := i32]}$
+```math
+\frac{<x, σ> ⇓ i32<e, σ> i32}{<x := i32, σ> ⇓ σ[x := i32]}
+```
 
 ```rust
 x = 1;
 ```
 Assignment bool expression
-
-$\frac{<x, σ> ⇓ bool<e, σ> bool}{<x := bool, σ> ⇓ σ[x := bool]}$
+```math
+\frac{<x, σ> ⇓ bool<e, σ> bool}{<x := bool, σ> ⇓ σ[x := bool]}
+```
 
 ```rust
 x = true;
@@ -443,8 +464,9 @@ For any assigment, the variable typed stored with the rhs evaluated type is chec
 
 
 Return i32
-
-$\frac{<f, σ>⇓σ}{<return : i32, σ> ⇓ σ[return : i32]}$
+```math
+\frac{<f, σ>⇓σ}{<return : i32, σ> ⇓ σ[return : i32]}
+```
 
 ```rust
 fn main() -> i32 {
@@ -455,8 +477,9 @@ The function is declared to return a type i32.
 
 
 Return bool
-
-$\frac{<f, σ>⇓σ}{<return : bool, σ> ⇓ σ[return : bool]}$
+```math
+\frac{<f, σ>⇓σ}{<return : bool, σ> ⇓ σ[return : bool]}
+```
 
 ```rust
 fn main() -> bool {
@@ -466,8 +489,9 @@ fn main() -> bool {
 The function is declared to return a type boolean.
 
 Void (none)
-
-$\frac{<f, σ>⇓σ}{<none, σ> ⇓ σ[none]}$
+```math
+\frac{<f, σ>⇓σ}{<none, σ> ⇓ σ[none]}
+```
 
 ```rust
 fn main() {
@@ -492,7 +516,9 @@ SOS rules of the type checker that has not been described above are the type che
 
 TO DISCUSS:
 Alternative answer would be to defined the SOS rules for functions as
-$<f, i32>⇓i32$, $<f, bool>⇓bool$, $<f, none>⇓none$. 
+```math
+<f, i32>⇓i32, <f, bool>⇓bool, <f, none>⇓none. 
+```
 
 The type checker will return a custom error with sufficient information except location e.g.
 ```rust