Commit 2026-09-10 11:06 a5c1af93

fix: macro_inline DFunLike instances to make Multiset.toFinsupp computable (#43620) This used to be computable, at least in 4.28.0. Something changed with the compiler that made it stop inlining these. macro_inline instruct the compiler to directly inline these at the callsite, which allows the unused typeclass arguments to be discarded immediately from the computability checker. Note that Coe already does this at the elaborator level, so this seems like a very reasonable thing to ask. The exhaustive application was performed by Gemini.