More underscores #3527
Merged
More underscores #3527
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
As suggested by Alexander van der Vekens, use math mode and a little text for a semiformal formula.
The character before the end of italics has to be alphanumeric. metamath-exe wasn't treating this as italics and latest metamath-knife was giving an error.
Because underscore is followed by ampersand, metamath-exe is not treating this as italics and latest metamath-knife is giving an error. Apparently we need to either give up the italics or give up the umlaut, and turning the umlaut into a following e is a pretty standard thing to do, so I guess we do that.
The intention here is a subscript and it turns out that is actually possible with no space between the backtick and the underscore.
This was referenced Sep 28, 2023
digama0
approved these changes
Sep 28, 2023
avekens
reviewed
Sep 28, 2023
| @@ -109155,7 +109155,7 @@ prove that every set is contained in a weak universe in ZF (see | |||
| of Formalized Mathematics, Vol 1, No 3, May-August 1990. A Tarski class | |||
| is a set whose existence is ensured by Tarski's axiom A (see ~ ax-groth | |||
| and the equivalent axioms). Axiom A was first presented in Tarski's | |||
| article _Über unerreichbare Kardinalzahlen_. Tarski introduced the | |||
| article _Ueber unerreichbare Kardinalzahlen_. Tarski introduced the | |||
There was a problem hiding this comment.
What'Äs the problem here with "_Über"?
There was a problem hiding this comment.
metamath-exe does not recognize _ as starting italics unless the next character is alphabetic
avekens
approved these changes
Sep 28, 2023
icecream17
reviewed
Sep 28, 2023
| @@ -625406,7 +625406,7 @@ family of sets (implicit). (Contributed by Stefan O'Rear, | |||
| over functions and points in N-dimensional space (which are equivalent | |||
| to functions from an "index set"). Many of the following theorems exist | |||
| to transfer standard facts about functions to elements of function | |||
| sets._ (Contributed by Stefan O'Rear, 30-Aug-2014.) (Revised by Stefan | |||
| sets_. (Contributed by Stefan O'Rear, 30-Aug-2014.) (Revised by Stefan | |||
There was a problem hiding this comment.
would this work? there is a period in the sentence before
There was a problem hiding this comment.
the ending underscore has to have a letter before it and no letter after it, so yes this should work
icecream17
approved these changes
Sep 28, 2023
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.
This is the followup for various issues discussed in #3521
With these changes I can successfully run
using the latest metamath-knife.