Zulip Chat Archive

Stream: general

Topic: has_reflect


view this post on Zulip Chris Hughes (Jun 14 2020 at 16:44):

Shouldn't this return T.t?

@[derive has_reflect] inductive T | t : T

def u : T := T.t

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

view this post on Zulip Rob Lewis (Jun 14 2020 at 17:49):

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

Last updated: May 11 2021 at 22:14 UTC