2,619
次編輯
「玩具語言的型別推理原則」修訂間的差異
無編輯摘要
Tankianting（討論 | 貢獻） （quad） |
Tankianting（討論 | 貢獻） |
||
| 行 6： | 行 6： | ||
#<math>\frac{x : STRUCT(name_0 : T_0, ..., name_n : T_n)\qquad{i = 0,1,\dots,n}}{x.item_i : T_i}</math> | #<math>\frac{x : STRUCT(name_0 : T_0, ..., name_n : T_n)\qquad{i = 0,1,\dots,n}}{x.item_i : T_i}</math> | ||
#<math>\frac{S = STRUCT(name_{S_0} : T_{S_0}, ..., name_{S_n} : T_{S_n})\qquad U = STRUCT(name_{U_0} : T_{U_0}, ..., name_{U_m} : T_{U_m}) \qquad m, n \in \mathbb{Z}^+ \qquad \forall i \in m\rightarrow name_{U_m} \in \{name_{S_j}\} \qquad n \ge m}{belongTo(S,U)}</math> | #<math>\frac{S = STRUCT(name_{S_0} : T_{S_0}, ..., name_{S_n} : T_{S_n})\qquad U = STRUCT(name_{U_0} : T_{U_0}, ..., name_{U_m} : T_{U_m}) \qquad m, n \in \mathbb{Z}^+ \qquad \forall i \in m\rightarrow name_{U_m} \in \{name_{S_j}\} \qquad n \ge m}{belongTo(S,U)}</math> | ||
#<math>\frac{x_i : X_i\qquad y : Y, i = 0,1,\dots , n}{(\lambda(x_0, \dots , x_n).y : (X_0, \dots , X_n | #<math>\frac{x_i : X_i\qquad y : Y, i = 0,1,\dots , n}{(\lambda(x_0, \dots , x_n).y) : (X_0, \dots , X_n)\rightarrow Y}</math> | ||
#<math>\frac{x_i : T_{x_i}\qquad n_i : T_{n_i}\qquad{belongTo(T_{x_i},~T_{n_i})}\qquad{i=0,1,...,m}\qquad{foo: ((T_{n_0}, \dots, T_{n_m})\rightarrow Y)}}{f(x_0,\dots, x_m) : Y}</math> | #<math>\frac{x_i : T_{x_i}\qquad n_i : T_{n_i}\qquad{belongTo(T_{x_i},~T_{n_i})}\qquad{i=0,1,...,m}\qquad{foo: ((T_{n_0}, \dots, T_{n_m})\rightarrow Y)}}{f(x_0,\dots, x_m) : Y}</math> | ||