Variable rule

PM[[ {Case (X_{1,i−1}^{⟶}, X_{i}, X_{i+1,n}^{⟶}) of ; | (P 1_{1,i−1}^{⟶}, Y_{1}, P 1_{i+1,n}^{⟶}) = E_{1} ; ⋮ ; | (P m_{1,i−1}^{⟶}, Y_{m}, P m_{i+1,n}^{⟶}) = E_{m}}]] =

\{ \begin{matrix}t = X_{i}; \\ t_{f} = PM[[ \{Case (X_{1,i−1}^{⟶}, X_{i+1,n}^{⟶}) of ; | (P 1_{1,i−1}^{⟶}, P 1_{i+1,n}^{⟶}) = E_{1}[t/Y_{1}]_{B} ; ⋮ ; | (P m_{1,i−1}^{⟶}, P m_{i+1,n}^{⟶}) = E_{m}[t/Y_{m}]_{B}\}]] \\ In t_{f} \} \end{matrix}

Irrefutable pattern rule

PM[[ {Case (X_{1,i−1}^{⟶} , X_{i} ,  X_{i+1,n}^{⟶}) of ; | (P 1_{1,i−1}^{⟶} , Y_{1} ,  P 1_{i+1,n}^{⟶}) = E_{1} ; ⋮ ; | (P k_{1,i−1}^{⟶} , Y_{k} ,  P k_{i+1,n}^{⟶}) = E_{k} ; | (P l_{l,i−1}^{⟶} , (Y l_{1} , Y l_{2}) , P l_{i+1,n}^{⟶}) = E_{l} ; ⋮ ; | (P m_{1,i−1}^{⟶} , (Y m_{1} , Y m_{2}) , P m_{i+1,n}^{⟶}) = E_{m}}]] =

{t_{1}, t_{2} = Detuple2 (X_{i});
t  = X_{i};
t_{f} = PM[[ {Case (X_{1,i−1}^{⟶} , t_{1} ,  t_{2} ,  X_{i+1,n}^{⟶}) of ; | (P 1_{1,i−1}^{⟶} , t_{1,1} , t_{1,2} , P 1_{i+1,n}^{⟶}) = E_{1}[t/Y_{1}]_{B} ; ⋮ ; | (P k_{1,i−1}^{⟶} , t_{k,1} , t_{k,2} , P k_{i+1,n}^{⟶}) = E_{k}[t/Y_{k}]_{B} ; | (P l_{l,i−1}^{⟶} , Y l_{1} , Y l_{2} , P l_{i+1,n}^{⟶}) = E_{l} ; ⋮ ; | (P m_{1,i−1}^{⟶} , Y m_{1} , Y m_{2} , P m_{i+1,n}^{⟶}) = E_{m}}]]

In t_{f}}

Refutable pattern rule

PM[[ {Case (X_{1,i−1}^{⟶} , X_{i} ,  X_{i+1,n}^{⟶}) of | (P 1_{1,i−1}^{⟶} , Nil ,  P 1_{i+1,n}^{⟶}) = E_{1} ⋮ | (P k_{1,i−1}^{⟶} , Nil ,  P k_{i+1,n}^{⟶}) = E_{k} | (P l_{l,i−1}^{⟶} , Y l_{1} : Y l_{2} , P l_{i+1,n}^{⟶}) = E_{l} ⋮ | (P m_{1,i−1}^{⟶} , Y m_{1} : Y m_{2} , P m_{i+1,n}^{⟶}) = E_{m}}]] =

List case (X_{i},

PM[[ {Case (X_{1,i−1}^{⟶} , X_{i+1,n}^{⟶}) of ; | (P 1_{1,i−1}^{⟶} , P 1_{i+1,n}^{⟶}) = E_{1} ; ⋮ ; | (P k_{1,i−1}^{⟶} , P k_{i+1,n}^{⟶}) = E_{k}}]],

\{ \begin{matrix}t_{h}, t_{t} = Cons 1 (X_{i}), Cons 2 (X_{i}); \\ t_{f} = PM[[ \{Case (t_{h} , t_{t} ,  X_{1,i−1}^{⟶} , X_{i+1,n}^{⟶}) of ; | (Y l_{1} , Y l_{2} , P l_{1,i−1}^{⟶} , P l_{i+1,n}^{⟶}) = E_{l} ; ⋮ ; | (Y m_{1} , Y m_{2} , P m_{1,i−1}^{⟶} , P m_{i+1,n}^{⟶}) = E_{m}\}]] \\ In t_{f}\} ) \end{matrix}

PM[[ \begin{matrix}\{Case & X & of \\ | & Y_{1} : Y_{2} & = E\}]] \end{matrix} = PM[[ \begin{matrix}\{Case & X & of \\ | & Y_{1} : Y_{2} & = E \\ | & Nil & = Error\}]] \end{matrix}

PM[[ \begin{matrix}\{Case & X & of \\ | & Nil & = E\}]] \end{matrix} = PM[[ \begin{matrix}\{Case & X & of \\ | & Nil & = E \\ | & t_{1} : t_{2} & = Error\}]] \end{matrix}

Mixed variable-refutable patterns

PM[[ \begin{matrix}\{Case & (X_{1}, & X_{2}, & X_{3} & ) & of \\ | & (Nil , & Y_{1,1} : Y_{1,2} , & Y_{1} & ) & = E_{1} \\ | & (Y_{2,1} : Y_{2,2} , & Y_{2} , & Nil & ) & = E_{2} \\ | & (Y_{3} , & Nil , & Y_{3,1} : Y_{3,2} & ) & = E_{3}\}]] = \end{matrix}

\{ \begin{matrix}t_{3}^{⟶} & = & X_{3}^{⟶}; \\ t_{f} & = & PM[[ \begin{matrix}\{Case & (X_{1}, & X_{2}, & X_{3} & ) & of \\ | & (Nil , & Y_{1,1} : Y_{1,2} , & Nil & ) & = E_{1}[t_{3}/Y_{1}]_{B} \\ | & (Nil , & Y_{1,1} : Y_{1,2} , & t_{1,1} : t_{1,2} & ) & = E_{1}[t_{3}/Y_{1}]_{B} \\ | & (Y_{2,1} : Y_{2,2} , & Nil , & Nil & ) & = E_{2}[t_{2}/Y_{2}]_{B} \\ | & (Y_{2,1} : Y_{2,2} , & t_{2,1} : t_{2,2} , & Nil & ) & = E_{2}[t_{2}/Y_{2}]_{B} \\ | & (Nil , & Nil , & Y_{3,1} : Y_{3,2} & ) & = E_{3}[t_{1}/Y_{3}]_{B} \\ | & (t_{3,1} : t_{3,2} , & Nil , & Y_{3,1} : Y_{3,2} & ) & = E_{3}[t_{1}/Y_{3}]_{B}\}]] \end{matrix} \\ In t_{f}\} \end{matrix}

Empty variable rule

PM[[ {Case () of ; | () = E_{1} ; ⋮ ; | () = E_{m}}]] = Compiler Error “overlapping patterns”

PM[[ \begin{matrix}\{Case & () & of \\ | & () & = E\}]] \end{matrix} = E