has_reflect

Stream: general

[Chris Hughes]

Shouldn't this return T.t?

@[derive has_reflect] inductive T | t : T

def u : T := T.t

#eval tactic.trace (reflect u) -- u

[Rob Lewis]

I think type class resolution has a special case for inferring reflected t instances when t is a ground term. You can work around this.

@[derive has_reflect] inductive T | t : T

def u : T := T.t

meta def trace_reflected (v : T) : tactic unit :=
tactic.trace $ reflect v

run_cmd tactic.trace (reflect u) -- u
run_cmd trace_reflected u -- T.t