_aux_Mathlib_Tactic_Have___elabRules_Mathlib_Tactic_tacticHave__1

Mathlib.Tactic.Have

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

Lean4

/-- An extension of the `have` tactic that turns the hypothesis into a goal to be proved later -/
@[tactic Mathlib.Tactic.tacticHave_]
public meta def _aux_Mathlib_Tactic_Have___elabRules_Mathlib_Tactic_tacticHave__1 : Lean.Elab.Tactic.Tactic✝ := fun
  | `(tactic| have$n:optBinderIdent $bs*$[ : $t:term]?) => do
    let (goal1, goal2) ← haveLetCore (← getMainGoal) n bs t false
    replaceMainGoal [goal1, goal2]
  | _ => no_error_if_unused% throwUnsupportedSyntax✝

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

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

Разделы

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

Аффилиация

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