_aux_Mathlib_Tactic_Have___elabRules_Mathlib_Tactic_tacticLet__1

Mathlib.Tactic.Have

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

Lean4

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

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

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

Разделы

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

Аффилиация

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