このエントリはIdris Advent Calendar 2020の19日目の記事です。 次はmock_beginnerさんでIdrisとはじめる型駆動開発です。

κeenです。今回はこのAdvent Calendarの山場の1つ、定理証明について解説しようと思います。

このエントリはIdris Advent Calendar 2020の18日目の記事です。

κeenです。Idrisで個人的に面白いなーと思ってる機能、 with 構文とそれを利用したViewについて紹介します。

このエントリはIdris Advent Calendar 2020の17日目の記事です。

κeenです。今回は小ネタとしてシンタックスシュガー（糖衣構文）やオーバーロードについて紹介します。 あとIdrisにはユーザが構文を拡張できる機能もあるのでそれも紹介します。

このエントリはML Advent Calendar 2020の21日目の記事です。 前はelpinalさんで「長さn以上のリストをファンクタで」、後はnymphuimさんで「OCaml の小ネタを書く」です。

κeenです。小ネタなんですが、SMLのDerived Formsについて書きます。

このエントリはIdris Advent Calendar 2020の16日目の記事です。

κeenです。今回はipkgを使ったIdrisのテストとCIを紹介していきます。CIはGitLab CIとGitHub Actions両方の設定を紹介します。

このエントリはIdris Advent Calendar 2020の15日目の記事です。

κeenです。今回はIdrisのドキュメントコメントとそれを使ったドキュメント生成ツールの使い方を紹介します。

このエントリはIdris Advent Calendar 2020の14日目の記事です。

κeenです。今回はIdrisのパッケージ機能とipkgについて説明します。

このエントリはIdris Advent Calendar 2020の13日目の記事です。

κeenです。 今回は座学パートとして標準ライブラリでよく使われてるけどまだ触れてない記法に触れていこうと思います。

このエントリはIdris Advent Calendar 2020 の12日目の記事です。

κeenです。今回は手を動かすパートとしてビットマップ画像の書き出しをIdrisでやってみます。 依存型やIdrisの標準ライブラリ、ファイルの扱いなどの練習になればなと思ってます。

このエントリはIdris Advent Calendar 2020の11日目の記事です。

κeenです。今回はIdrisの複数のファイルだとか標準ライブラリだとかを扱おうと思います。