diff --git a/design/calculus_rules.typ b/design/calculus_rules.typ
index 51c9deb..d7ec505 100644
--- a/design/calculus_rules.typ
+++ b/design/calculus_rules.typ
@@ -8,7 +8,7 @@
   body
 }
 
-#let mk-box(title, body, ..args) = box(
+#let mk-box(title, body, ..args) = block(
   inset: 1em,
   stroke: black,
   ..args,
@@ -23,12 +23,25 @@
   colspan: c
 )[]
 
-#mk-box(width: 60%)[Syntax][
+#let tab = sym.arrow.r.stop
+#let nl = move(dx: -2pt, dy: 2pt, sym.arrow.curve.l)
+#let syntax-preamble = doc => {
+  show tab: set text(fill: gray.darken(20%))
+  show sym.arrow.curve.l: set text(fill: gray.darken(20%))
+  set math.cases(gap: 4pt)
+
+  show math.equation: set align(left)
+
+  doc
+}
+
+#let python-syntax = mk-box(width: 100%)[Python Syntax][
+  #show: syntax-preamble
   #grid(
     columns: (auto, auto, 1fr, auto),
-    align: (left, left, left, right),
+    align: (left, left, left, right).map(a => a + horizon),
     column-gutter: .4em,
-    row-gutter: 1em,
+    row-gutter: 1.2em,
     $"t"$, $::=$, none, [_terms_],
     blank(11, 2),
     $"x"$, [_variable_],
@@ -55,13 +68,56 @@
     grid.cell(colspan: 4)[],
 
     $"s"$, $::=$, none, [_statements_],
-    blank(3, 2),
+    blank(4, 2),
     $"x" = "t"$, [_assignment_],
     $"x": "T"$, [_variable declaration_],
-    $#syntax[def] f("x": "T") -> "T": "t"$, [_def_],
+    $ cases(
+      #syntax[def] f("x": "T") -> "T": #nl,
+      #tab "t" #nl,
+      delim: "["
+    ) $, [_def_],
+    $ cases(
+      #syntax[if] "t": #nl,
+      tab "s" #nl,
+      #syntax[else]: #nl,
+      tab "s" #nl,
+      delim: "["
+    ) $, [_if / else_],
   )
 ]
 
+#let midas-syntax = mk-box(width: 100%)[Midas Syntax][
+  #show: syntax-preamble
+  #grid(
+    columns: (auto, auto, 1fr, auto),
+    align: (left, left, left, right).map(a => a + horizon),
+    column-gutter: .4em,
+    row-gutter: 1.2em,
+    $"T"$, $::=$, none, [_types_],
+    blank(5, 2),
+    $"X"$, [_named type_],
+    $"T" ["T"]$, [_type application_],
+    $"T" #syntax[where] "c"$, [_constraint type_],
+    ${attach("p"_i: "T"_i, tr: i in 1..n)}$, [_complex type_],
+    $(attach("a"_i: "T"_i, tr: i in 1..n)) -> "T"$, [_function type_],
+    grid.cell(colspan: 4)[],
+
+    $"s"$, $::=$, none, [_statements_],
+    blank(2, 2),
+    $#syntax[type] "X" = "T"$, [_type definition_],
+    $#syntax[type] "X"["Y"] = "T"$, [_generic definition_],
+  )
+]
+
+#grid(
+  columns: (1fr, 1fr),
+  column-gutter: 1em,
+  python-syntax,
+  midas-syntax
+)
+
+#pagebreak()
+
 #let abs-typ-rules = (
   int: rule($Gamma tack "i": "Int"$, name: [(T-Int)]),
   float: rule($Gamma tack "f": "Float"$, name: [(T-Float)]),
@@ -81,7 +137,7 @@
   ),
   call: rule(
     $Gamma tack f: "T"_1 -> "T"_2$,
-    $Gamma tack "t" -> "T"_1$,
+    $Gamma tack "t": "T"_1$,
     $Gamma tack f("t"): "T"_2$,
     name: [(T-Call)]
   ),
@@ -109,6 +165,13 @@
     $Gamma tack "x": "T" tack.l Gamma, "x": "T"$,
     name: [(T-Annot)]
   ),
+  if-else: rule(
+    $Gamma tack "t": "Bool"$,
+    $Gamma tack "s"_1 tack.l Gamma'$,
+    $Gamma tack "s"_2 tack.l Gamma''$,
+    $Gamma tack #syntax[if] "t": "s"_1 #syntax[else]: "s"_2 tack.l Gamma$,
+    name: [(T-IfElse)]
+  )
 )
 
 #let py-typ-rules = (
@@ -131,6 +194,12 @@
   ternary: ```py (true if cond else false): T ```,
   op: ```py (a + b): T```,
   annot: ```py x: T```,
+  if-else: ```py
+    if cond:
+      ...
+    else:
+      ...
+  ```,
 )
 
 #let reading-keys = (
@@ -139,10 +208,13 @@
   ],
   annot: [
     _Gamma_ judges that $"x": "T"$ adds $"x": "T"$ to the context
+  ],
+  if-else: [
+    _Gamma_ judges that $#syntax[if] "t": "s"_1 #syntax[else]: "s"_2$ produces an the unchanged context $Gamma'$, iff _Gamma_ judges that $"t": "Bool"$, that $"s"_1$ produces the context $Gamma'$, and $"s"_2$ produces the context $Gamma''$. This means that statements in 
   ]
 )
 
-#mk-box[Typing][
+#mk-box[Python Typing][
   #v(1em)
   #stack(dir: ltr, spacing: 1fr)[_*Rule*_][_*Python example*_]