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