Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Move real-related materials out of iterateTheory #1245

Merged
merged 3 commits into from
May 31, 2024

Conversation

binghe
Copy link
Contributor

@binghe binghe commented May 24, 2024

Hi,

This PR intends to make the iterateTheory a more fundamental theory without theorems about real numbers. The theory file is now moved to src/pred_set/src/more_theories, while the previous real-related materials of iterateTheory are moved into the existing real_sigmaTheory. This introduced a small incompatibility which can be fixed by opening real_sigmaTheory in addition to iterateTheory.

This changes paves the way for the abstract algebra materials to open iterateTheory for doing ring arithmetics (sum), etc. without having realTheory in ancestry, thus is important for some future work (on algebra materials).

--Chun

@binghe binghe changed the title Move real-related theorem out of iterateTheory Move real-related materials out of iterateTheory May 24, 2024
@mn200 mn200 merged commit fe6fe54 into HOL-Theorem-Prover:develop May 31, 2024
4 checks passed
@binghe binghe deleted the iterateTheory branch June 7, 2024 01:07
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants