これは「Idris Advent Calendar 2020 - Qiita」の6日目の記事です。 Idris で自然数の加法の交換法則を証明してみましょう。 以下のように Comm.idr を書いて、ロードします。 関数commの型だけを書いた状態です。 %default totalはおまじないだと思ってくだ…