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: Nov 11 2024 at 04:22 UTC