Jibiana Jakpor (Apr 10 2026 at 05:08): Jibiana Jakpor (Apr 10 2026 at 05:08):Hello, I am having an issue with an abbreviation not being contracted in the output window. str_substr always remains expanded as in the following example:
Even stranger, other abbreviations from the same theory do get contracted. I saw a warning in the thread #Beginner Questions > Not to expand abbreviation in proof state that locales can keep abbreviations from being folded in, but the abbreviation was not declared in a locale. What do you think could be the problem?
Mathias Fleury (Apr 10 2026 at 05:27):n >= 0 vs 0 <=n
Mathias Fleury (Apr 10 2026 at 05:27):the former is expanded to the latter during parsing
Mathias Fleury (Apr 10 2026 at 05:27):so your abbreviation needs to be written with 0 <= n
Mathias Fleury (Apr 10 2026 at 05:28):(this is an educated guess, because you did not show the abbreviation...)
Jibiana Jakpor (Apr 10 2026 at 05:35):That was exactly the issue. This helps me a lot. Thank you so much!
Notification Bot (Apr 10 2026 at 05:36):Jibiana Jakpor has marked this topic as resolved.
Last updated: Apr 14 2026 at 09:21 UTC