_aux_Mathlib_Tactic_CongrExclamation___elabRules_Congr!_congr!_1

Mathlib.Tactic.CongrExclamation

URI: https://scilib.ai/kg/mathlib#Congr!._aux_Mathlib_Tactic_CongrExclamation___elabRules_Congr!_congr!_1

Lean4

@[tactic Congr!.congr!]
public meta def _aux_Mathlib_Tactic_CongrExclamation___elabRules_Congr!_congr!_1 : Lean.Elab.Tactic.Tactic✝ := fun
  | `(tactic| congr!$cfg:optConfig$[ $n]?$[ with $ps?*]?) => do
    let config ← elabConfig cfg
    let patterns := (Lean.Elab.Tactic.RCases.expandRIntroPats (ps?.getD #[])).toList
    liftMetaTactic fun g ↦
        let depth := n.map (·.getNat)
        g.congrN! depth config patterns
  | _ => no_error_if_unused% throwUnsupportedSyntax✝

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

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

Разделы

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

Аффилиация

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