このエントリは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の複数のファイルだとか標準ライブラリだとかを扱おうと思います。

このエントリはRust 2 Advent Calendar 2020の10日目の記事です。 前は mocyutoさんでRustでEC2検索を簡単にするCLIの作り方 - Screaming Loud、
後は mas-yoさんでRustでstaticなEntity Component System - Qiitaでした

空いてる日を埋める担当のκeenです。 気付いたら空きができてたので埋めます。 Rustのリリースノートなどでよくみる const fn についてです。

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

κeenです。 今回はIdrisで簡単な競技プログラミングの問題を解いてみたいと思います。

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

κeenです。Idrisのインタフェースやモナドについて紹介します。

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

κeenです。昨日の予告通り今回は手を動かすパートとしてIdrisのREPLを紹介することにします。

κeenです。 以前雑な実装でブログにOGP画像を生成するようにしましたが、禁則処理が気になったのでそれを工夫したときの記録です。