2,617
次編輯
「型別理論與形式證明筆記」修訂間的差異
跳至導覽
跳至搜尋
→2.7 well-typedness 於lambda→
Tankianting（討論 | 貢獻） |
Tankianting（討論 | 貢獻） |
||
| 行 261： | 行 261： | ||
但是若是z是β，則無法得知其型別，換言之，是illegal的。這種well-typedness推論有不同的推論方法。 | 但是若是z是β，則無法得知其型別，換言之，是illegal的。這種well-typedness推論有不同的推論方法。 | ||
== 2.8-2.10 == | |||
參[[:檔案:型別理論與形式證明筆記Sec2.8-2.10.pdf|此pdf]]。 | |||
=附註：本筆記使用的邏輯推演排版法= | =附註：本筆記使用的邏輯推演排版法= | ||