Bryan Gin-ge Chen
Bryan Gin-ge Chen
moved per Mario's suggestion.
There's [`conv.interactive.apply_congr`](https://github.com/leanprover-community/mathlib/pull/2221) as of a few days ago.
I did some bisection and the example from the OP doesn't crash with Lean 3.10.0c and does crash with Lean 3.11.0c. I suspect #211 again, see also #372 and the...
I think this is an [elan](https://github.com/Kha/elan/) issue, and it may have been fixed with the recently released 0.8.0.
It should be fine as long as the code that initializes the emscripten build (around [here](https://github.com/leanprover-community/lean/blob/ec1613aef1eee72e601f192b16740629c6d49690/src/shell/lean_js.cpp#L38) I think) is updated to use the correct option.
@rwbarton No problem, just ping me again in the PR.
Another example: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/buggy.20infoview.3F
This crash occurs because of a null pointer dereference here: https://github.com/leanprover-community/lean/blob/master/src/library/inductive_compiler/ginductive.cpp#L240 When I run the debug build of Lean, I get a "LEAN ASSERTION VIOLATION" here: https://github.com/leanprover-community/lean/blob/master/src/library/equations_compiler/elim_match.cpp#L760 (And indeed, line...
Do you happen to have any tips: e.g. what I could evaluate in the debugger to find out? Entering `expr x_type` in `lldb` returns some `m_ptr` addresses which I don’t...
I'm having a hell of a time getting `gdb` to work properly on macOS. That aside, I'm not sure how this function `process_constructor_core` works so I don't know that I'll...