Can't display a number wrapped in a structure

Stream: new members

[Mike Shulman]

The following code:

structure wrap := (t : Type)
def wrapN : wrap := { t := ℕ }
def x : wrapN.t := (0 : ℕ)
#eval x

complains that result type does not have an instance of type class 'has_repr', dumping internal representation and prints #0. Is there a way to make this print something nicer, short of reimplementing has_repr by hand for the structure wrapN?

[Eric Wieser]

Reimplementing has_repr by hand is about one line of work:

instance : has_repr wrapN.t := nat.has_repr

[Eric Wieser]

attribute [reducible] wrapN is also enough to make this work

[Mike Shulman]

But I have to do it for every instance of wrap?

[Eric Wieser]

This feels like an #xy problem

[Alex J. Best]

What do you mean by instance of wrap (instance is a keyword) are you varying wrapN or the class?

[Eric Wieser]

Also your title is misleading; your code example isn't a number wrapped in a struct, this is a type wrapped in a struct which typeclass resolution can't see though.

[Eric Wieser]

A "number wrapped in a struct" would be

structure wrap (t : Type) := (val : t)
def x : wrap  ℕ := wrap.mk 0