Zulip Chat Archive

Stream: general

Topic: multiple solutions for typeclass search

view this post on Zulip 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