elab_proxy_equiv

Mathlib.Tactic.ProxyType

URI: https://scilib.ai/kg/mathlib#Mathlib.ProxyType.elab_proxy_equiv

Lean4

/-- Elaborator for `proxy_equiv%`. -/
@[term_elab proxy_equiv]
def elab_proxy_equiv : Elab.Term.TermElab := fun stx expectedType? =>
  match stx with
  | `(proxy_equiv% $t) => do
    let (type, indVal) ← elabProxyEquiv t expectedType?
    let config : ProxyEquivConfig := ProxyEquivConfig.default indVal
    ensureProxyEquiv config indVal
    mkAppOptM config.proxyEquivName (type.getAppArgs.map some)
  | _ => throwUnsupportedSyntax

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

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

Разделы

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

Аффилиация

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