misc + iota axiom saves #4492
Merged
misc + iota axiom saves #4492
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
icecream17
force-pushed
the
develop
branch
2 times, most recently
from
24b760d to
d6f17c9
Compare
jkingdon
approved these changes
Dec 27, 2024
There was a problem hiding this comment.
My suggestions are non-blocking.
The only thing in here which really caught my eye was the changes to iota related theorems. If someone who has thought more about iota than I has an opinion, speak up. If not, I think we can go with these changes, as they seem like improvements in terms of axiom usage.
jkingdon
reviewed
Dec 27, 2024
|
|
benjub
reviewed
Dec 28, 2024
matches recent changes to ~ el and ~ dtru
rgenw + ss2rab + mpbir = a1i + ss2rabi ralrimivw + ss2rab + sylibr = adantr + ss2rabdv Ideally ss2rabi and ss2rabdv would be renamed with an "a" suffix, then new ss2rabi and ss2rabdv would be made. For now it is implemented manually but it is equivalent to an automatic shortening. mptexgf: a1i + ss2rabi scottex: adantr + ss2rabdv wwlksnfi: a1i + ss2rabi disjxwwlkn: a1i + ss2rabi occon: adantr + ss2rabdv rmxyelqirr: (more extensive) itgoss: adantr + ss2rabdv ovnsslelem: adantr + ss2rabdv (+auto minimize) ovolval5lem3: a1i + ss2rabi (+auto minimize) ---- Add ss2ab1 and ss2abdv to mathbox, shorten abssdv
dfopifOLD no longer uses ax-10 to 12 so it is restored
rebase: changes-set.txt, iotauni2 now uses unisnv
benjub
approved these changes
Dec 29, 2024
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Commit by commit (a lot more compartmentalized than my last pr)
About 40 to 50 miscallaneous downstream axiom saves are from the first few commits, and then iotaval/iotaex is responsible for the rest in the axiom diff.