_aux_Mathlib_Tactic_Lift___elabRules_Mathlib_Tactic_lift_1

Mathlib.Tactic.Lift

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

Lean4

@[tactic Mathlib.Tactic.lift]
public meta def _aux_Mathlib_Tactic_Lift___elabRules_Mathlib_Tactic_lift_1 : Lean.Elab.Tactic.Tactic✝ := fun
  | `(tactic| lift $e to $t$[ using $h]?$[ with $newVarName$[ $newEqName]?$[ $newPrfName]?]?) =>
    withMainContext <|
      let keepUsing :=
        match h, newPrfName.join with
        | some h, some newPrfName => h.raw == newPrfName
        | _, _ => false
      Lift.main e t h newVarName newEqName.join keepUsing
  | _ => no_error_if_unused% throwUnsupportedSyntax✝

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

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

Разделы

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

Аффилиация

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