きゅーけー@tojoqk@mastodon.tojo.tokyo: Agda で開発していた日付ライブラリの Gregorianum、一旦ここで開発を完了していいかと思い始めた。<br><a class="link-in-note" href="https://github.com/tojoqk/gregorianum" target="_blank" rel="nofollow noopener">https://github.com/tojoqk/gregorianum</a><br><br>今後は本来の目的である、org-mode 上で Agda のコードを文芸的に記述し、睡眠記録の入力を Agda のコンストラクタの追加で実現するという目的の実現へと移ろう。そのために、時刻を扱う必要があるけどそこはそんなに一般的な感じにならないからライブラリにはしないでいいやっていう感じ。

Home | Notifications | New Note | Local | Federated | Search | Logout

Note Detail

きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-04-13 20:14:25)
Agda で開発していた日付ライブラリの Gregorianum、一旦ここで開発を完了していいかと思い始めた。
https://github.com/tojoqk/gregorianum

今後は本来の目的である、org-mode 上で Agda のコードを文芸的に記述し、睡眠記録の入力を Agda のコンストラクタの追加で実現するという目的の実現へと移ろう。そのために、時刻を扱う必要があるけどそこはそんなに一般的な感じにならないからライブラリにはしないでいいやっていう感じ。