Update HOME_EXAM.md

HOME_EXAM.md

@@ -93,7 +93,6 @@ Program
 ```ebnf
 Function
     :"fn" Id "(" (Arg ",")* Arg? ")" "->" Type BlockExpr
-    |"fn" Id "()" "->" "()" BlockExpr
     ;
 ```
 
@@ -443,7 +442,7 @@ Let statements works in a similiar way.
 
 ##### Functioncall
 ```math
-\frac{(<e_1,σ> → n_1 ... <e_i,σ> → n_i) → σ(arg1 := n_1, ..., argi := n_i))}{<c,σ> → (x,σ')}; \text{where x is the return value}
+\frac{(<e_1,σ> → n_1 ... <e_i,σ> → n_i) → σ[arg_1 := n_1, ..., arg_i := n_i]}{<f.c,σ> → (v,σ')}; \text{where v is the return value}
 ```
 
 ```rust
@@ -561,7 +560,7 @@ fn b() -> bool {
 
 ##### Conditional command
 ```math
-\frac{<e,σ> → \text{ bool } <c0,σ> → t}{<\text{ if e then } c0 \text{ else } c1,σ> → t}, \text{ where t = type of last statement }
+\frac{<e,σ> → \text{ bool } <c0,σ> → t <c1,σ> → t}{<\text{ if e then } c0 \text{ else } c1,σ> → t}, \text{ where t = type of last statement }
 ```
 
 For the if statement to go through the type checker need the expression, e, be a boolean.
@@ -592,7 +591,7 @@ The example above is valid for the type checker due to it only checking that the
 
 ##### Functioncall
 ```math
-\frac{<e_1,σ> → t_1 ... <e_i,σ> → t_i}{<c,σ> → t-res}, \text{ where } t-res = \text{return type of function } 
+\frac{<e_1,σ> → t_1 ... <e_i,σ> → t_i σ[arg_1 == t_1, ..., arg_i == t_i]}{<f.c,σ> → f.t}, \text{ where } f.t = \text{return type of function } 
 ```
 
 Each expression evaluating to the same type as the arguments connected to the function.