Skip to content

Make renumbering of proof derivation steps optional#45

Open
abchugh wants to merge 1 commit intodigama0:masterfrom
abchugh:master
Open

Make renumbering of proof derivation steps optional#45
abchugh wants to merge 1 commit intodigama0:masterfrom
abchugh:master

Conversation

@abchugh
Copy link

@abchugh abchugh commented Jul 14, 2020

Sophize is using this function to get proofs in a format that can imported. Thus, renumbering needs to be avoided for this case.

Sophize is using this function to get proofs in a format that can imported. Thus, renumbering  needs to be avoided for this case.
@digama0
Copy link
Owner

digama0 commented Jul 14, 2020

It looks like this is still renumbering though, just with a different numbering scheme? Perhaps the constants should be exposed as RunParms instead.

@abchugh
Copy link
Author

abchugh commented Jul 14, 2020

I am calling this function in a separate piece of code (outside MMJ2) where I call the function with the value false. RunParms can also help but I want to disable this renumbering completely.

@abchugh
Copy link
Author

abchugh commented Jul 14, 2020

I realize that I should have given you more context:
I am using this function here:
https://github.com/Sophize/METAMATH_SERVER/blob/master/src/main/java/org/sophize/metamath/resourcewriter/ResourceStore.java#L258

I copy-paste all code from mmj2 to this repo. I would like to remove hacks I made and make mmj2 code identical in the two repos.

@abchugh
Copy link
Author

abchugh commented Jul 16, 2020

Gentle ping!

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.

2 participants