2,619
次編輯
「型別理論與形式證明筆記」修訂間的差異
→2.4 Church lambda→演算的推演規則 (derivation rules)
Tankianting（討論 | 貢獻） |
Tankianting（討論 | 貢獻） |
||
| 行 130： | 行 130： | ||
注意上面的符號，逗號,表示連結上下文。上下文<math>\Gamma</math>可以為空。 | 注意上面的符號，逗號,表示連結上下文。上下文<math>\Gamma</math>可以為空。 | ||
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去。 | ||