赴成功高中宣傳

幸好沒斷氣 XD。表定時間是 12:20 ~ 13:10，但輔導室老師一來就跟我們說大概 12:30 才能開始 XD。鄭老師先用他一貫的閒聊語氣從就業、創意（還有鄭老師最愛的 Google XD）那些路線切入，接著輪我講很「理性」的編程樂趣，然後另一位同學講點資訊系的生活，最後有獎徵答。結束時已經 13:15 了，沒時間讓他們問問題真是可惜。（I was expecting "deep" questions XD. ）活動看起來很正式，一開始有感謝狀給老師，要結束的時候連校長都來了！人還算滿多的，而且主要是小高一。高中生現在真的連在學校裡面都不扎衣服了耶！

雖然骨幹沒變（不然就搭不上投影片了 XD），但大概有 30% ~ 40% 是脫稿演出吧 XD。我發現站到人前自然就講得出來了，可能是以前有經驗的關係。總之我把台下的小朋友（輔導室老師是這麼稱呼他們的 XD）視為 rational beings（最重要的原則！），企圖向他們傳達編程所帶來的「理性的感動」（？）。小朋友們也相當捧場，連我講「看看資訊系是搞什麼飛機的 ─ 當然我們不搞飛機」這種東西都有 50% 的笑聲耶 XD。（我講的時候大概就笑這一次 XD。）總之給這麼少時間，大概就只能講這樣吧，希望我的目標有成功啦。但鄭老師說得好，這種宣傳的效果實在沒辦法評估 XD。

回台大的時候搭鄭老師的便車。老師問到研究所，我就很猶豫不知道怎麼回答啦。因為我提到修數學系的課，老師就問我是對什麼有興趣，我就把 scm 老師、program derivation 和 dependent types 搬出來，用的例子當然是「產生所有 permutations 再拿一個排序好的出來」XD。（這是 functional specification 啦，講這個比較快 XD。）scm 老師找來的幫手突然動了好多（兩個人都好強…），可是我今天還要寫圖論作業和 DSD 期中考卷… 明天！Agda programmming 就排在明天！我這次一定要弄懂怎麼搞那個小黑點 XD。

--
其實如果能變成 squiggolist 好像很不錯耶 XD。

---

把 ordered? 寫成 relational fold 好像只有形式上漂亮，實際上在做 pattern matching 的時候很痛苦…因為 inductive case 裡面關於 ordered? 的部份展開後會變成這種東西

其中 lbound ? 還是用 set coreflexive 的方法下去做的，經過那裡的時候又更恐怖 XD。

--
有好方法嗎？

---

多用一點 with 好像不錯 XD。

--
不小心開始寫了 XD。