Post #1782144

@screwlisp wrote: «ACL2 has an extended version, acl2(r) that uses nonstandard analysis to provide the reals. (Er, I think this means that you provide a function that rationally converges toward the real number from below, and then you plus a nonstandard number onto the series if the real number is irrational).» Thank you. Non-standard, as in Robinson's? A close encounter with ACL2 is the next thing I have to leave for another time, alas. @simon_brooke