I’ve seen a big topic regarding typeclasses being whether or not they should be bundled or unbundled. Over time I’ve found that you can actually pull off doing them both at the same time and getting the best of both worlds! I mad a gist showing it off here: Using Bundled and Unbundled Typeclasses Simultaneously in Coq · GitHub
1 Like