2,728
次編輯
「型別理論與形式證明筆記」修訂間的差異
跳至導覽
跳至搜尋
無編輯摘要
Tankianting（討論 | 貢獻） |
Tankianting（討論 | 貢獻） |
||
| 行 131： | 行 131： | ||
注意上面的符號，逗號,表示連結上下文。上下文<math>\Gamma</math>可以為空。 | 注意上面的符號，逗號,表示連結上下文。上下文<math>\Gamma</math>可以為空。 | ||
1. | 1.變數沒有前提，只有conclusion，可以用在推演開頭，意思是在上下文內的變數可以從這個上下文推演出來。 | ||
因為我們在conclusion（結論）不需要<math>x</math>在左邊的上下文，所以3.抽象的<math>x:\sigma</math>被移到<math>\vdash</math>右邊的statement去。 | 因為我們在conclusion（結論）不需要<math>x</math>在左邊的上下文，所以3.抽象的<math>x:\sigma</math>被移到<math>\vdash</math>右邊的statement去。 | ||