elabCHoleExpand

Mathlib.Tactic.TermCongr

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.TermCongr.elabCHoleExpand

Lean4

@[term_elab cHoleExpand, inherit_doc cHoleExpand]
def elabCHoleExpand : Term.TermElab := fun stx expectedType? =>
  match stx with
  | `(cHole% lhs$h) => elabCHole h true expectedType?
  | `(cHole% rhs$h) => elabCHole h false expectedType?
  | _ => throwUnsupportedSyntax

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

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

Разделы

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

Аффилиация

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