「型別理論與形式證明筆記」修訂間的差異

無編輯摘要
行 11: 行 11:


# 型別變數:<math display="inline">\alpha \in {\mathbb{V}} \Rightarrow  \alpha \in {\mathbb{T}}</math>,表達基本型別,比如list, nat等
# 型別變數:<math display="inline">\alpha \in {\mathbb{V}} \Rightarrow  \alpha \in {\mathbb{T}}</math>,表達基本型別,比如list, nat等
# 箭頭型別:<math display="inline">\alpha,\tau \in {\mathbb{T}}  (\alpha \Rightarrow \tau) \in {\mathbb{T}}</math>
# 箭頭型別:<math display="inline">\alpha,\tau \in {\mathbb{T}} \Rightarrow (\alpha \arrow \tau) \in {\mathbb{T}}</math>


箭頭<math display="inline">\rightarrow</math>是右結合的,和函數的apply代入不同。比較<math display="inline">\alpha \rightarrow \beta \rightarrow \gamma = \left( \alpha \rightarrow (\beta \rightarrow \gamma) \right)</math>和<math display="inline">x_{1}x_{2}x_{3} = \left( \left( x_{1}x_{2} \right)x_{3} \right)</math>。
箭頭<math display="inline">\rightarrow</math>是右結合的,和函數的apply代入不同。比較<math display="inline">\alpha \rightarrow \beta \rightarrow \gamma = \left( \alpha \rightarrow (\beta \rightarrow \gamma) \right)</math>和<math display="inline">x_{1}x_{2}x_{3} = \left( \left( x_{1}x_{2} \right)x_{3} \right)</math>。


[[category:資訊]]
[[category:資訊]]