1 Answers
In type theory a typing environment represents the association between variable names and data types.
More formally an environment Γ {\displaystyle \Gamma } is a set or ordered list of pairs ⟨ x , τ ⟩ {\displaystyle \langle x,\tau \rangle } , usually written as x : τ {\displaystyle x:\tau } , where x {\displaystyle x} is a variable and τ {\displaystyle \tau } its type.
The judgement
is read as " e {\displaystyle e} has type τ {\displaystyle \tau } in context Γ {\displaystyle \Gamma } ".
4 views
Answered