jrh13
jrh13
I really like the principle, but am a bit nervous about the resource usage running it in CI. Currently the hol-light repo only uses whatever is provided in a free...
Thank you all, I'll now consider this one closed.
This terminological inconsistency is certainly confusing. It was actually a little result in my PhD thesis that the two things are equivalent (a chapter discusses this reals construction). I'll tweak...
Yes indeed, now closed
This looks like a very helpful sanity check, thank you! Since `CHECK_VARTYPES_TAC` is bound at the top level, perhaps it is worth adding a `Help/CHECK_VARTYPES_TAC.hlp` file for it?