2023.10.11
https://gyazo.com/0e177ee7bb15e9addcd1da6fca76630c
前：
2023.10.10
後：
2023.10.12
#日報
はい
#デジタルの日
2
やった?
命題論理の
シークエント計算
を
Lean 4
で形式化しようとしている，が…
例えば
高さ0の証明木を作るルールは
$ \rm Init
と
$ \rm L\bot
しかないので，これら2通りについて考えれば良い
みたいなものをどう
Lean 4
で書けば良いのかよくわからない．