Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] A::pcpo , datatype B = Cons A . Is B::pcpo?

Email Gateway (Aug 22 2022 at 12:58):

From: Jonathan Woodgate via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hello,
is there an elegant way to show that B is also a PCPO? (since Cons is bijective)

Thank you!

Last updated: Apr 20 2024 at 01:05 UTC