Inferenz für Let

(alles ganz analog zu Auswertung von Ausdrücken)

• Regeln für Umgebungen
  • E[v : = t] $$\vdash$$ v : t
  • $${\frac{{E \vdash v' : t'}}{{E[v:=t] \vdash v' : t'}}}$$ für v≠v'
• Regeln für Bindung:
  $${\frac{{E\vdash X : s, \quad E [v:=s] \vdash Y : t}}{{E \vdash \mathtt{let } v=X \mathtt{ in } Y : t}}}$$