Now I'm even more interested in learning Lean 🤩
so you can say “here’s what it means to be a sorting algorithm” and mark it as typeclass, and write code against it. and then separately you can have different instances of that typeclass that actually provide the code, and control which one it’s resolved to
0 reposts1 like