背景 最近、輪読会でIdrisの勉強をしました。 教材はプログラング言語Idrisに入門させたい（v0.9）を使ったのですが、ド・モルガンの法則等の証明はとても興味深かったです。 証明を書くことで、単体テスト等で確認していたことがコンパイラで賄える点は非常に便利だと感じま...