2024.01.20
https://www.youtube.com/watch?v=1Gb2ET99M3k
イワシがつちからはえてくるんだ
の
トキポナ
前：
2024.01.19
後：
2024.01.21
#日報
観た
ソードアート・オンライン
1期
思った
明確な言語仕様があるのなら
lojban
の文法規則を全部
Lean 4
などの
定理証明支援系
上に実装するみたいなことも出来るのだろうか？
https://twitter.com/SnO2WMaN/status/1748441767194903015
適当に文を入れたときそれが
lojban
として適切な文法なのかをチェックする検証器を作るみたいな試みを想定していた．（
定理証明支援系
に載せる意義があるのかはわからない）
思った
ソードアート・オンライン
の
ナーヴギア
，もし何も起きずに普通にゲームが開始したとしてトイレどうする予定だったんだろう？
空腹感はわかるはず（1話）なのでおそらく排泄欲も感じるはず．
通知とかが来るらしいし，緊急時には強制ログアウトの手筈だったらしい．