Email Gateway (Aug 18 2022 at 11:24): Email Gateway (Aug 18 2022 at 11:24):From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi all,
I have a lemma valid_unconc, that has a variable c of list type.
Now I want to get a specialized version where c is a singleton list.
I tried
lemmas valid_uncons = valid_unconc[where c="[s]", simplified]
but this will give a lemma where s is fixed, rather then a schematic
variable ("...[s]..." instead of "...[?s]...").
The following seems to work, but I don't understand why or what else it
would do if there occurred pair types in my lemma:
lemmas valid_uncons =
valid_unconc[where c="[s]", simplified, split_format]
So is this the way to go, or is there another way to specialize a lemma
as I want to do?
Thanks in advance for any hints,
Peter
Email Gateway (Aug 18 2022 at 11:25):From: Makarius <makarius@sketis.net>
Just add the "standard" attribute to the pipe-line.
It is often better to avoid such in-situ transformations of facts
altogether, which are slightly unreadable and also happen to interact
badly with local theory contexts (facts "in" a locale or class context
etc.).
Makarius
Last updated: May 03 2024 at 12:27 UTC