[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] I don't like predicative Dedekind cuts. You have to add rules for the algebraic operations... Archimedean ordered rational integral domains... category: redirected to nlab