Commit 2025-01-23 21:13 764d7e76

feat: add fast_instance% elaborator (#11521) Quoting the docstring: fast_instance% inst takes an expression for a typeclass instance inst, and unfolds it into constructor applications that leverage existing instances. For instance, when used as

instance instSemiring : Semiring X := sorry
instance instRing : Ring X := fast_instance% Function.Injective.ring ..

this will define instRing as a nested constructor application that refers to instSemiring. The advantage is then that instRing.toSemiring unifies almost immediately with instSemiring, rather than having to break it down into smaller pieces. Related to #7432