Comment Comment by ToValueFunfetti This has happened: https://github.com/leanprover/lean4/issues/14576 parent ToValueFunfetti 1 month ago