# 终章，Lambda演算建模——程序即证明！

| categories academic

type ::= primitive | function | ( type )
primitive ::= A | B | C | D | ...
function ::= type -> type


• A implies B implies A
• (A implies B implies C) implies ((A implies B) implies (A implies C))

（任何正常人看完会说“什么？”，但，我显然不是正常人，我是一个数学怪咖。）

If you liked this post, you can share it with your followers !