能力範圍之外

Patrik Jansson 又加了好多意見，而且我覺得好像一些主要的弱點被打到了，像

• Patrik 說 idR⊒foldR inductive case 的 pattern matching 很複雜，我在證 isort-der 的時候比這複雜好幾倍，所以就用很多層的 with 慢慢把 pattern 一層一層拆開，不過只好讀一點點而已；
• 把 permute 精煉成 fold 所用的 combine 本來是直接給定義（因為是參考 R.S. Bird 的 paper），但 Patrik 覺得他比較想看到怎麼為了滿足 fusion condition 而把 combine 的定義湊出來；
• 如果我們還不知道 derivation 的結果，就用 Agda mode 互動地寫的話，真的會那麼順利嗎？這篇 paper 的證明都是知道結果之後一次把整個 derivation 寫下來，但是真的要一步步地湊一個證明出來似乎有問題；
• 然後最後一個 comment 我覺得有些酸味… 也可能是我太敏感。

這種程度的問題憑我是應付不來的… 現在只能寄望 scm 老師再變變魔術，把它弄得四平八穩 XD。我愈來愈覺得排在第二位很不安 XD。

--
不知道 scm 老師現在雲遊到何方了 XD。