こわくない Idris (6) - M59のブログ こわくない Idris (6) - M59のブログ 1年前に書いた記事を読み返していたら、証明がすぐには理解できなかった。証明の内容を言葉で分かるように書いておきたいと思う。次のコードのMyHead.headは、全域函数だ。 %default…