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

跳至導覽 跳至搜尋
行 47: 行 47:
型別變數 type variable:<math display="inline">{\mathbb{V}} = \left\{ \alpha,\beta,\gamma,\ldots \right\}</math>用希臘字母表示。
型別變數 type variable:<math display="inline">{\mathbb{V}} = \left\{ \alpha,\beta,\gamma,\ldots \right\}</math>用希臘字母表示。


<math display="inline">\mathbb{T}</math>:所有簡單型別,定義如下:
<math display="inline">{\mathbb{T}}</math>:所有簡單型別,定義如下:


# 型別變數:<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等

導覽選單