Mac Malone
Mac Malone
After a long debugging session (including with `gdb`), it appears that the root olean (and only the root olean) handle stays open for some reason on Windows. This causes the...
It is also worth noting that MSYS2 `rm` can remove the olean but `IO.FS.removeFile` cannot.
To elaborate on the problem here a bit: there are empty closed terms in `main`, so the underlying problem is similar to #1965. ```lean set_option trace.compiler.ir.result true in def main...
The `where` style just seems like a waste of space. It never disambiguates anything, right?
@david-christiansen If the `where` is useless, doesn't it make the most sense to deprecate that style? I suspect the only reason core primarily uses it is because at one point...
@austinletson Yep, #4608 seems exactly like what we want here! I left a code review with a few suggested tweaks over there. Also, mentioning the default workflow behavior in the...
One potential type-class-based solution that eliminates the need for `throwThe` at the cost of losing support for implicit-type `.` constructors (e.g., `throw (.userError "hi")` would have to be written as...