Lean4
/-- The term elaborator `derive_fintype% α` tries to synthesize a `Fintype α` instance
using all the assumptions in the local context; this can be useful, for example, if one
needs an extra `DecidableEq` instance. It works only if `α` is an inductive
type that `proxy_equiv% α` can handle. The elaborator makes use of the
expected type, so `(derive_fintype% _ : Fintype α)` works.
This uses `proxy_equiv% α`, so as a side effect it defines `proxyType` and `proxyTypeEquiv` in
the namespace associated to the inductive type `α`.
-/
@[term_parser 1000]
public meta def «termDerive_fintype%_» : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Deriving.Fintype.«termDerive_fintype%_» 1022
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "derive_fintype% ") (ParserDescr.cat✝ `term 0))
