戰意

Haskell-cafe 一個討論串突然拐到 dependent types 來，有人寫了一小段 Coq 證明 length (map f (xs ++ ys)) = length xs + length ys，駁斥「dependently-typed languages 裡的證明都極為冗長、寫起來很煩」的說法。看到 Coq 不知所云的證明（XD）頓時不知從哪裡湧出一股戰意：Agda 的證明漂亮得多呀！Agda 有直覺的 proof terms 和美麗的 mixfix unicode operators，造就了人人稱讚的 equational reasoning combinators，Coq 怎麼比呀！

很快就意識到這種情緒實在太不邏輯了，顯然是因為 Coq 的 pi-calculus code 裡面用上千行 tactics 堆起來的證明不用 coqide 看就看不懂的緣故 XD。

--
顯然今天沒辦法實現新策略 XD。