Deriving Repr for an inductive with proof parameters

Stream: new members

[Graham Leach-Krouse]

Here's something a bit confusing:

inductive test1 : Type where
  | wrap : 2 < 3 → test1
  deriving Repr

structure test2 : Type where
  wrap : 2 < 3
  deriving Repr

a Repr instance is derivable for test2, but not test1. Is there an idiomatic way to rewrite test1, keeping it as an inductive type (in the real-world case there might be other constructors), but making Repr derivable? Ideally it would be nice to do this without adding an auxiliary structure like test2 just for wrapping purposes.

[Kyle Miller]

Thanks for the report. lean4#3944 has a fix