Email Gateway (Jan 31 2021 at 01:55): Email Gateway (Jan 31 2021 at 01:55):From: "David E. Narvaez" <den9562@rit.edu>
Greetings,
I need to use the fact that
sorted_list_of_fset {||} = []
This would have been as simple as having
lemmas sorted_list_of_fset_empty =
sorted_list_of_set_empty[Transfer.transferred]
if the FSet theory, but since this (rather obvious piece) is missing as of
Isabelle 2020, I now need to prove it in my theory, but the transfer method
does not seem to work:
setup_lifting type_definition_fset
lemma "sorted_list_of_fset {||} = []"
proof (transfer)
How can I achieve this?
Last updated: Jul 15 2022 at 23:21 UTC