このエントリはIdris Advent Calendar 2020の24日目の記事です。
前はhiropon21さんでSnocList recursive viewを型駆動開発してみよう in Idris2 でした。
Idris2は1と比べて型システムが微妙に変わっており、ところどころ 0 a のようにその値を使える回数が表示されていたりしますね。
κeenです。今回はIdrisのFFIとCodegenについて触れたいと思います。
このエントリはIdris Advent Calendar 2020の22日目の記事です。
κeenです。今回は依存型を使って部分的に正しさを証明したデータ構造を作っていきたいと思います。 慣れてない人には難しめの内容になるかもしれません。
このエントリはIdris Advent Calendar 2020の21日目の記事です。 前はmock_beginnerさんでIdrisとはじめる型駆動開発でした。
κeenです。大ネタが続いたのでそろそろ小ネタでも。文芸的プログラミングの機能です。
このエントリは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について説明します。