Liam O'Connor (Apr 28 2023 at 02:43): Liam O'Connor (Apr 28 2023 at 02:43):Hi all, I think this counts as a beginner question although I'm not a beginner.
I am working with the Complete_Partial_Order theory (https://isabelle.in.tum.de/library/HOL/HOL/Complete_Partial_Order.html)
And I want to make function types an instance of the ccpo class if their result is (via pointwise lifting):
instantiation "fun" :: (type, ccpo) ccpo
begin
But, annoyingly, because the Complete_Partial_Order theory imports Complete_Lattices, and there is such an instance for complete lattices, and all complete lattices are complete partial orders, there already is an instance for "fun", just for "fun" :: (type, complete_lattice) complete_lattice.
I don't want this type class instance, because the ccpo I want to work with is not a complete lattice. Can I remove this instance somehow? Or is there some way to replace it with a more general one?
Last updated: Apr 27 2024 at 20:14 UTC