Lean4
/-- The term elaborator `proxy_equiv% α` for a type `α` elaborates to an equivalence `β ≃ α`
for a "proxy type" `β` composed out of basic type constructors `Unit`, `PLift`, `Sigma`,
`Empty`, and `Sum`.
This only works for inductive types `α` that are neither recursive nor have indices.
If `α` is an inductive type with name `I`, then as a side effect this elaborator defines
`I.proxyType` and `I.proxyTypeEquiv`.
The elaborator makes use of the expected type, so `(proxy_equiv% _ : _ ≃ α)` works.
For example, given this inductive type
```
inductive foo (n : Nat) (α : Type)
| a
| b : Bool → foo n α
| c (x : Fin n) : Fin x → foo n α
| d : Bool → α → foo n α
```
the proxy type it generates is `Unit ⊕ Bool ⊕ (x : Fin n) × Fin x ⊕ (_ : Bool) × α` and
in particular we have that
```
proxy_equiv% (foo n α) : Unit ⊕ Bool ⊕ (x : Fin n) × Fin x ⊕ (_ : Bool) × α ≃ foo n α
```
-/
@[term_parser 1000]
public meta def proxy_equiv : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.ProxyType.proxy_equiv 1022
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "proxy_equiv% ") (ParserDescr.cat✝ `term 0))
