コラッツ予想がとけたらいいな その4

[0412 １３２人目の素数さん 2023/08/24(木) 08:30:04.42 ID:9r4b23w8]

>>411
いえ、Lean 4 の制約かもしれません。
数をパターンマッチしているのではなく、SingleLimited でマッチをかけているので、
「型」の上では正常動作するけど、実行はできないのかもしれません。