See discussion on #846 (comment) -- it would be nice to collect lemmas like
lemma virqType_eq[simp]:
"virqType = virq_type"
into one theory in Refine that is included relatively early.
This would help to consolidate, make sure we're using a consistent simp direction for these and potentially mark them for sharing between the specs directly.
Main problem is how to find them all.
See discussion on #846 (comment) -- it would be nice to collect lemmas like
into one theory in Refine that is included relatively early.
This would help to consolidate, make sure we're using a consistent
simpdirection for these and potentially mark them for sharing between the specs directly.Main problem is how to find them all.