Oskar Abrahamsson
Oskar Abrahamsson
Won't this PR need an update now that #1002 has been merged?
The error comes from these: https://github.com/HOL-Theorem-Prover/HOL/blob/develop/src/HolSat/sat_solvers/minisat/Global.h#L264. I don't know what this nonsense is and I suspect you could safely delete the definitions within the #ifdef, but you could try to...
But `'a misc_app_list * 'a misc_app_list` is a _pair_ of two `'a misc_app_list`s?
You will have to switch between write and exec after you write new code, but I don’t remember the details. But this should explain it: https://developer.apple.com/documentation/apple-silicon/porting-just-in-time-compilers-to-apple-silicon
The language in the paper is lazy and pure. Will these rewrites hold in a strict language with side effects?
I think you should consider targeting purecake with this sort of thing, and not CakeML. The reason is that I suspect that these sort of rewrites enable things like ```...