Notification Bot (Apr 10 2026 at 19:17): Notification Bot (Apr 10 2026 at 19:17):Jibiana Jakpor has marked this topic as unresolved.
Jibiana Jakpor (Apr 10 2026 at 23:15):I am also having trouble with this abbreviation
abbreviation str_indexof:: "uc_word ⇒ uc_word ⇒ int ⇒ int" where
"str_indexof w v i ≡ (if 0 ≤ i ∧ (str_contains (str_substr w i ¦w¦) v) ∧ i≤¦w¦ then Int.int (indexof_nat w v (Int.nat i)) else -1)"
Here is it how it appears in the proof state:
Kevin Kappelmann (Apr 11 2026 at 15:00):This might not be the answer you want, but: This shouldn't be an abbreviation anyway but a definition. Then you prove the characteristic theorems you need about the definition and never unfold it again.
Jibiana Jakpor (Apr 12 2026 at 21:57):That is a good point. In this case, I'm not the author of this formalization, and I think that abbreviations might have been important for the original use case the authors had in mind. I don't want to break backwards compatibility, so I'm hesitant to replace the abbreviations with definitions.
Mathias Fleury (Apr 13 2026 at 05:01):When you cannot change the definition, the only way is to compare the terms exactly to see what the difference really is. Here it looks like ¦w¦ is different from int (length w)
Mathias Fleury (Apr 13 2026 at 05:02):In some cases like this in the past, I have introduced a str_indexof' version that was what could be applied
Last updated: Apr 14 2026 at 09:21 UTC