Oliver Nash (Nov 08 2020 at 11:34):
I'm wondering how evil, if at all, the following pattern is:
class foo := (x : ℕ) def bar [foo] : ℕ := foo.x def baz (f : foo) := bar instance foo_inst : foo := ⟨37⟩ lemma bar_val : bar = 37 := rfl lemma baz_val (f : foo) : baz f = f.x := rfl
The point is that
baz_val is true only because typeclass search first looks for the nearby argument
f before it heads off to look for registered instances. So is the correctness of this lemma due only to an implementation detail of typeclass search, or is this a feature which it is valid to exploit?
Last updated: May 16 2021 at 05:21 UTC