lean4-htt/tests/leanpkg/deriving/UserDeriving.lean