feat: upstream `ToExpr` deriving handler from Mathlib - #6473

Merged

kmill merged 4 commits into

leanprover:masterfrom

kmill:derive-toExpr

Dec 31, 2024

Commits on Dec 27, 2024

feat: Upstream derive handler for `ToExpr` from Mathlib

alexkeizer
authored and
kmill
committed
b023dac

Commits on Dec 29, 2024

sort out universe level handling
kmill
committed
51d6b6f
small change
kmill
committed
1599c23

Commits on Dec 30, 2024

comments, formatting
kmill
committed
48966fd