Lukas Stevens (Jul 17 2020 at 14:09): Lukas Stevens (Jul 17 2020 at 14:09):I have the theorem x < y ⟷ x ≤ y ∧ ¬ (x = y). The term of that theorem (Thm.prop_of) gets automatically changed to x < y ⟷ x ≤ y ∧ x ≠ y. This term is used as a key in a Termtab. Later, I manually build a term that is of the first form, but because of the contracted abbreviation it is not found in the table. Is there any way to prevent that contraction?
Lukas Stevens (Jul 17 2020 at 14:15):Is it possible that the pretty-printing is just fooling me?
Manuel Eberl (Jul 17 2020 at 14:29):How do you get hold of these terms in the first place?
Lukas Stevens (Jul 17 2020 at 14:29):Ah, the problem is that the type does not match apparently.
Manuel Eberl (Jul 17 2020 at 14:29):It is somewhat unusual to have a term where abbreviations have not yet been unfolded.
Manuel Eberl (Jul 17 2020 at 14:29):yeah that seems more likely
Lukas Stevens (Jul 17 2020 at 14:33):It was confusing because I printed several terms with a TERM exception and one term had the abbreviation contracted while the other term didn't.
Manuel Eberl (Jul 17 2020 at 14:49):btw you can also print terms with Pretty.writeln/Syntax.pretty_term.
Manuel Eberl (Jul 17 2020 at 14:49):or, even more easily, convert them to a cterm and do @{print}
Manuel Eberl (Jul 17 2020 at 15:11):of course that might sometimes obscure some things, so in those cases you can just @{print} the term directly to see what it looks like in ML
Manuel Eberl (Jul 17 2020 at 15:12):but that is /very/ verbose, so I'd only do that for very small terms
Last updated: Apr 25 2024 at 12:23 UTC