elabProdAssoc

Mathlib.Tactic.ProdAssoc

URI: https://scilib.ai/kg/mathlib#Lean.Expr.elabProdAssoc

Lean4

/-- Elaborator for `prod_assoc%`. -/
@[term_elab prodAssocStx]
def elabProdAssoc : TermElab := fun stx expectedType? => do
  match stx with
  | `(prod_assoc_internal%) =>
    do
      let some expectedType ← tryPostponeIfHasMVars? expectedType? |
        throwError"expected type must be known"
      let .app (.app (.const ``Equiv _) a) b := expectedType |
        throwError "Expected type{indentD expectedType}\nis not of the form `α ≃ β`."
      mkProdEquiv a b
  | _ =>
    throwUnsupportedSyntax

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru