Skip to content
Snippets Groups Projects
Commit 682b680a authored by Hugo Wangler's avatar Hugo Wangler
Browse files

Update HOME_EXAM_Type_check_part2.md

parent 1ef53028
No related branches found
No related tags found
No related merge requests found
...@@ -70,52 +70,52 @@ or ...@@ -70,52 +70,52 @@ or
``` ```
Not equals (!=): Not equals (!=):
$` math```
\frac{\Gamma \ \vdash \ e1 \ : \ bool \quad \Gamma \ \vdash \ e2 \ : \ bool}{\Gamma \ \vdash (e1 \ != \ e2) \ : \ bool} \frac{\Gamma \ \vdash \ e1 \ : \ bool \quad \Gamma \ \vdash \ e2 \ : \ bool}{\Gamma \ \vdash (e1 \ != \ e2) \ : \ bool}
`$ ```
or or
$` math```
\frac{\Gamma \ \vdash \ e1 \ : \ i32 \quad \Gamma \ \vdash \ e2 \ : \ i32}{\Gamma \ \vdash (e1 \ != \ e2) \ : \ bool} \frac{\Gamma \ \vdash \ e1 \ : \ i32 \quad \Gamma \ \vdash \ e2 \ : \ i32}{\Gamma \ \vdash (e1 \ != \ e2) \ : \ bool}
`$ ```
### Assignment ### Assignment
Given the type $`\tau`$, variable $`x`$ and value $`n`$ Given the type $`\tau`$, variable $`x`$ and value $`n`$
$` math```
\frac{\Gamma \ \vdash \ x \ : \ \tau \quad \Gamma \ \vdash \ n \ : \ \tau}{\lang x := n, \sigma \rang \ \Darr \ \Gamma \ \vdash x \ : \ \tau} \frac{\Gamma \ \vdash \ x \ : \ \tau \quad \Gamma \ \vdash \ n \ : \ \tau}{\lang x := n, \sigma \rang \ \Darr \ \Gamma \ \vdash x \ : \ \tau}
`$ ```
### **let** assignment ### **let** assignment
$` math```
\frac{\Gamma \ \vdash \ n \ : \ \tau}{\lang \text{let} \ x \ : \ \tau \ := \ n, \sigma \rang \ \Darr \ \Gamma \ \vdash x \ : \ \tau} \frac{\Gamma \ \vdash \ n \ : \ \tau}{\lang \text{let} \ x \ : \ \tau \ := \ n, \sigma \rang \ \Darr \ \Gamma \ \vdash x \ : \ \tau}
`$ ```
### **while** statement ### **while** statement
The condition, $`b`$, of the while statement The condition, $`b`$, of the while statement
$` math```
\frac{}{\Gamma \ \vdash b \ : \ bool} \frac{}{\Gamma \ \vdash b \ : \ bool}
`$ ```
### **if/elseif** statement ### **if/elseif** statement
The conditions, $`b_i`$, of the if- and elseif-statements The conditions, $`b_i`$, of the if- and elseif-statements
$` math```
\frac{}{\Gamma \ \vdash b_i \ : \ bool} \frac{}{\Gamma \ \vdash b_i \ : \ bool}
`$ ```
### Functions ### Functions
Given the function $`p`$ with the type of its return type Given the function $`p`$ with the type of its return type
$` math```
\frac{\Gamma \ \vdash p \ : \ \tau \quad \lang p, \sigma \rang \ \Darr \ n}{\Gamma \ \vdash n \ : \ \tau} \frac{\Gamma \ \vdash p \ : \ \tau \quad \lang p, \sigma \rang \ \Darr \ n}{\Gamma \ \vdash n \ : \ \tau}
`$ ```
#### Parameters and arguments #### Parameters and arguments
Given a function with parameters $`p1, \dotsb, p_i`$ and arguments $`a1, \dotsb, a_i`$ then for every parameter and argument Given a function with parameters $`p1, \dotsb, p_i`$ and arguments $`a1, \dotsb, a_i`$ then for every parameter and argument
$` math```
\frac{\Gamma \ \vdash p_i \ : \ \tau}{\Gamma \ \vdash a_i \ : \ \tau} \frac{\Gamma \ \vdash p_i \ : \ \tau}{\Gamma \ \vdash a_i \ : \ \tau}
`$ ```
\ No newline at end of file \ No newline at end of file
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment