きゅーけー@tojoqk@mastodon.tojo.tokyo: グレゴリオ歴の日付を形式的に扱うためのAgdaのライブラリの開発が一区切りついたのでGitHubに公開した。 型で閏年から月ごとに日数の違い、そして日付の隣接関係を扱えているのですごい。 コンパイルした時点で日付のバグ発生しないといえるように設計できた。 とくに Day 型の構造がうまくできていて、「月末」を型として完全に表現できるようになっている。 <a class="link-in-note" href="https://github.com/tojoqk/gregorianum/tree/main" target="_blank" rel="nofollow noopener">https://github.com/tojoqk/gregorianum/tree/main</a>

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

Note Detail

きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-02-23 10:35:52)
グレゴリオ歴の日付を形式的に扱うためのAgdaのライブラリの開発が一区切りついたのでGitHubに公開した。
型で閏年から月ごとに日数の違い、そして日付の隣接関係を扱えているのですごい。
コンパイルした時点で日付のバグ発生しないといえるように設計できた。

とくに Day 型の構造がうまくできていて、「月末」を型として完全に表現できるようになっている。

https://github.com/tojoqk/gregorianum/tree/main
---Attachments---
image: https://mastodon.tojo.tokyo/system/media_attachments/files/116/117/358/014/620/043/original/efd6233ef1c1f79b.png
image: https://mastodon.tojo.tokyo/system/media_attachments/files/116/117/358/019/064/779/original/16c43c11c4c1ff83.png
image: https://mastodon.tojo.tokyo/system/media_attachments/files/116/117/358/020/537/171/original/fdf250f4e05ee9be.png