From cd40b83e9febfc6dc795a932d78171b034fe517a Mon Sep 17 00:00:00 2001 From: Hugo Wangler <hugwan-6@student.ltu.se> Date: Fri, 22 Nov 2019 13:14:55 +0000 Subject: [PATCH] Add new file --- HOME_EXAM_Type_check_part3.md | 39 +++++++++++++++++++++++++++++++++++ 1 file changed, 39 insertions(+) create mode 100644 HOME_EXAM_Type_check_part3.md diff --git a/HOME_EXAM_Type_check_part3.md b/HOME_EXAM_Type_check_part3.md new file mode 100644 index 0000000..37d1733 --- /dev/null +++ b/HOME_EXAM_Type_check_part3.md @@ -0,0 +1,39 @@ +### Assignment +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} +``` + +### **let** assignment +```math +\frac{\Gamma \ \vdash \ n \ : \ \tau}{\lang \text{let} \ x \ : \ \tau \ := \ n, \sigma \rang \ \Darr \ \Gamma \ \vdash x \ : \ \tau} +``` + +### **while** statement +The condition, $`b`$, of the while statement + +```math +\frac{}{\Gamma \ \vdash b \ : \ bool} +``` + +### **if/elseif** statement +The conditions, $`b_i`$, of the if- and elseif-statements + +```math +\frac{}{\Gamma \ \vdash b_i \ : \ bool} +``` + +### Functions +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} +``` + +#### Parameters and arguments +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} +``` \ No newline at end of file -- GitLab