2022.07.24
https://www.youtube.com/watch?v=3dv_T1sUkhI
前：2022.07.23
後：2022.07.25
#日報
思った
tasty(テストフレームワーク)，名前testyで良いだろ
いいね
Musikk Per Automakkdonald's
https://www.youtube.com/watch?v=3dv_T1sUkhI
涙
安福さん(sm38295182)
https://nicothumb2img.vercel.app/image/sm38295182#.png https://nico.ms/sm38295182
観た
リコリス・リコイル 第4話
100点！！！！
面白すぎて2回見ちゃった（照）
やった
Idris2（Idris）入門
型は命題である
code:sample.idr
OneIsOne : Type
OneIsOne = (1 = 1)
OneIsTwo : Type
OneIsOne = (1 = 2)
OneIsOneOrTwo : Type
OneIsOneOrTwo = Either OneIsOne OneIsTwo
OneIsOneAndTwo : Type
OneIsOneAndTwo = Pair OneIsOne OneIsTwo
$ A \lor B: Either A B
$ A \land B: Pair A B
$ \forall a \in A. P(a): (a: A) -> P a
$ \exists a \in A. P(a): (a: A ** P a)
$ \lnot A: Not a
ただしNot a = a -> Void
$ \lnot A := A \vdash \bot
開発環境がとんでもなく重くなったので断念
読んだ
火遊び同盟
病弱少女の口が悪いと…嬉しい！！という、正直な気持ち
https://twitter.com/SnO2WMaN/status/1550968976532189184
絵がだいすきすぎ
話もだいすきすぎ
知った
ゆかりんと茜ちゃんの証明ゲームLeanプレイ講座 #1【定理証明支援系】(動画)
https://www.nicovideo.jp/watch/sm40432561
LeanのVOICEROID実況　すごすぎる
邪神ちゃんドロップキック Xの初音ミクって結局藤田 咲本人なのか初音ミクそのものなのかわからなかったけど海外版でも普通に初音ミクなので初音ミクだということがわかった
Marshmello ft. Bastille - Happier (Slowed + Reverb)
https://www.youtube.com/watch?v=En7g5Nthm6M
Slowed + Reverbって本人がやっていいんだ
思った
Haskell難しすぎる！！！
DenoのURL importってIPFSにも対応してるのか？
多分してない
されていると嬉しいことってなんだろうか　
いいね
ういにゃん - ニコニコ老人会リミックスメドレー
https://www.youtube.com/watch?v=BSIG2hCGF70