repeat' を使用すると並列場合分けができる？

lean-ja / lean-by-example

コード例で学ぶ Lean 言語

https://lean-ja.github.io/lean-by-example/

MIT License

39 stars 7 forks source link

Closed Seasawher closed 3 months ago

Seasawher commented 3 months ago

要検証

Seasawher commented 3 months ago

ドモルガン iff 弱い排中律の証明で必要な並列場合分けをどうやるかという話

all_goalsだと「場合分けで生じたゴール」に適用できない

タクティク結合子を使うと横にどんどん長くなってしまう

repeat か repeat' でできないか？試してみたい

Seasawher commented 3 months ago

むり