Every suc is a free name

盯著這兩條規則看，一陣子後得到結論 ─ 名字的傳遞要分開處理。自從為 Proc type 加上一個 natural number index n 表示有 n 個 free names 之後，情況似乎滿樂觀，已解決規則的 side conditions 都自然地表達在 encoding 裡面。De Bruijn index 和「把 context 編在 type 裡面」的手法湊在一起，就有了一句口號：給我一個 suc，我就送你一個免費的名字 XD。

今日飲食：中午沙茶豬肉麵 @ 男一麵食部（$50）；晚上鍋燒烏龍麵 @ 老爺上菜（$80）+ 巧克力葡萄奶酥麵包 @ 男一麵包店（$18）。合計 $148。

--
應該有人觀察出規律了吧？XD