Idris Advent Calendar 2020 3日目の記事です。 2020年今年の言語に Idris を選んで年始に Hello, World していたのですが、見事にその後 Python をしていた1年でした（仕事で使うことになったので Python を覚える必要が出てきました）。 完全に Idris は初…