2,619
次編輯
「型別理論與形式證明筆記」修訂間的差異
跳至導覽
跳至搜尋
→附註：本筆記使用的邏輯推演排版法
Tankianting（討論 | 貢獻） |
Tankianting（討論 | 貢獻） |
||
| 行 164： | 行 164： | ||
</pre> | </pre> | ||
範例： | |||
<pre> | |||
*y : α → β* | |||
| *z : α* | |||
| | y : α → β | |||
| | z : α | |||
| | y z: β | |||
| λz.(y z): α → β | |||
λy.λz.(y z): (α → β) → α → β | |||
</pre> | |||
[[category:資訊]] | [[category:資訊]] | ||