3 ms·

I'm reading https://leanprover.github.io/theorem_proving_in_lean/type_classes.html https://leanprover.github.io/theorem_proving_in_lean/type_cl... but I'm not s

• firstlink 4y ago
  I can't figure out what you mean by "coherent" in this context. ETA: Oh, if you mean like rust trait coherence, then no. That would map to instances being unique, which is not the case. In addition to being able to pass arbitrary values as instance parameters, there is a priority system. But some effort is put into making sure that alternate implementations end up defeq, which is kind of like uniqueness in a way.