[acl2/acl2] 904acf: Begin the development of reals in set theory via D...

[MattKaufmann]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 904acf589841f19d190da616dde7ffd2b96d7da2
https://github.com/acl2/acl2/commit/904acf589841f19d190da616dde7ffd2b96d7da2
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2026-07-01 (Wed, 01 Jul 2026)

Changed paths:
A books/projects/set-theory/reals/dedekind.lisp
A books/projects/set-theory/reals/negative.lisp
A books/projects/set-theory/reals/sum.lisp

Log Message:
-----------
Begin the development of reals in set theory via Dedekind cuts.

I've defined Dedekind cuts and their sum and negative, proving that
sum and negative preserve the property of being a Dedekind cut.
Proving this for the negative case was getting messy, so I got AI to
help as described in file
books/projects/set-theory/reals/negative.lisp.



To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications

[acl2buildserver]

Branch: refs/heads/testing