getType''

Mathlib.Lean.Meta

URI: https://scilib.ai/kg/mathlib#Lean.MVarId.getType''

Lean4

/-- Get the type the given metavariable after instantiating metavariables and cleaning up
annotations. -/
def _root_.Lean.MVarId.getType'' (mvarId : MVarId) : MetaM Expr :=
  return (← instantiateMVars (← mvarId.getType)).cleanupAnnotations

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

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

Разделы

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

Аффилиация

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