κeenです。ゴールデンウィークに買ったマシンがややトラブルありつつも組み上がって安定稼動しはじめたのでメモを残します。

κeenです。お久しぶりですね。表題のとおり入社報告です。

このエントリはIdris/Idris2 Advent Calendar 2022の1日目の記事として過去に遡って投稿しています。

κeenです。ぼちぼちIdris2を触りはじめたので小出しに色々なことを書いていきます。今回はIdris2のインストーラ兼パッケージマネージャ兼ビルドツールのpackについて

κeenです。最近気が向いたときにInkscapeでスライドを作るようにしてるんですが、できあがったPDFの置き場に困ってたのでPDFをインラインで表示できるようにしたお話です。

κeenです。なんか証明しづらいなって思ってたところをコード側を書き直したらすんなりいけたのでメモ。

κeenです。某勉強会の準備で色々Idrisのライブラリを眺めてたら面白いものを見付けたので共有します。 依存型があればどの言語でも定義できるはずですが、標準添付ライブラリとしてIdris2に入ってたのでタイトルにIdris2を入れときました。

κeenです。先日ついうっかりbtrfsのファイルシステムをdisk fullにしてしまったので、そこからリカバリしたときの記録を残しておきます。