2023.06.12
https://gyazo.com/abd309f461e49ec9121b677b359c5fc8
前：
2023.06.11
後：
2023.06.13
#日報
やった
ひさびさに
Lean 4
を
やった
Skolem化
について振り返る
メモ
原始再帰
$ \mathrm{prec}_{f,g}(\lang l,r\rang):\N \to \N
$ \lang l,0 \rang
のとき
$ f(l)
$ \lang l,r+1\rang
のとき
$ g(r,\mathrm{prec}_{f,g}(\lang l,r\rang))