This is for the anonymous function indicated by $⟨$match$\mathrm{⟩}$. $⟨$match$\mathrm{⟩}$ is of the form

  $\mathrm{⟨}$pat${}_{\mathrm{1}}$$\mathrm{⟩}$ => $\mathrm{⟨}$exp${}_{\mathrm{1}}$$\mathrm{⟩}$
| $\mathrm{\cdots }$
| $\mathrm{⟨}$pat${}_n$$\mathrm{⟩}$ => $\mathrm{⟨}$exp${}_n$$\mathrm{⟩}$

that indicates pairs of an argument pattern and its corresponding function body.

The type of each pair of a pattern and expression $⟨$pat${}_i$$\mathrm{⟩}$ =¿ $⟨$exp${}_i$$\mathrm{⟩}$ is calculated as follows: first, the type $⟨$ty${}_i$$\mathrm{⟩}$ of $⟨$pat${}_i$$\mathrm{⟩}$ is calculated; second, under the environment extended with variables in the pattern, the type $⟨$ty${}^{\mathrm{\prime }}{}_i$$\mathrm{⟩}$ of $⟨$exp${}_i$$\mathrm{⟩}$ is calculated; and finally, the two types are combined into a function type $\mathrm{⟨}$ty${}_i$$\mathrm{⟩}$ -> $\mathrm{⟨}$ty${}^{\mathrm{\prime }}{}_i$$\mathrm{⟩}$. The type of this entire expression is $\mathrm{⟨}$ty$\mathrm{⟩}$ -> $\mathrm{⟨}$ty’$\mathrm{⟩}$ that is obtained by unifying the types of the matching pairs. The value of this function is the function closure consisting of the current value environment and the function expression itself.