From the paper "Haskell-style type classes with Isabelle/Isar", type classes not only allow for simple overloading but form a generic calculus, an instance of order-sorted algebra
I wonder whether there exists some theory about the OSA.
Thanks a lot
Last updated: Feb 01 2025 at 20:19 UTC