synthesizeUsingTactic

Mathlib.Util.SynthesizeUsing

URI: https://scilib.ai/kg/mathlib#synthesizeUsingTactic

Lean4

/-- `synthesizeUsing type tacticSyntax` synthesizes an element of type `type` by evaluating the
given tactic syntax.

Example:
```lean
let (gs, e) ← synthesizeUsingTactic ty (← `(tactic| congr!))
```

The tactic `tac` is allowed to leave goals open, and these remain as metavariables in the
returned expression.
-/
def synthesizeUsingTactic {u : Level} (type : Q(Sort u)) (tac : Syntax) : MetaM (List MVarId × Q($type)) := do
  synthesizeUsing type
      (do
        evalTactic tac)

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

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

Разделы

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

Аффилиация

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