termProd_assoc% — Mathlib

Lean4
/-- `prod_assoc%` elaborates to the "obvious" equivalence between iterated products of types,
regardless of how the products are parenthesized.
The `prod_assoc%` term uses the expected type when elaborating.
For example, `(prod_assoc% : (α × β) × (γ × δ) ≃ α × (β × γ) × δ)`.

The elaborator can handle holes in the expected type,
so long as they eventually get filled by unification.
```lean
example : (α × β) × (γ × δ) ≃ α × (β × γ) × δ :=
  (prod_assoc% : _ ≃ α × β × γ × δ).trans prod_assoc%
```
-/
@[term_parser 1000]
public meta def «termProd_assoc%» : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Lean.Expr.«termProd_assoc%» 1024 (ParserDescr.symbol✝ "prod_assoc%")
Похожие утверждения