Lean4
/-- `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
```lean
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`
rather than applications of `Function.Injective.ring` or other non-canonical constructors.
The advantage is then that `instRing.toSemiring` unifies almost immediately with `instSemiring`,
rather than having to break it down into smaller pieces.
-/
@[term_parser 1000]
public meta def fastInstance : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Elab.FastInstance.fastInstance 1022
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "fast_instance%") (ParserDescr.cat✝ `term 0))
