_aux_Mathlib_Tactic_Polyrith___elabRules_Mathlib_Tactic_Polyrith_tacticPolyrithOnly[_]_1

Mathlib.Tactic.Polyrith

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Polyrith._aux_Mathlib_Tactic_Polyrith___elabRules_Mathlib_Tactic_Polyrith_tacticPolyrithOnly[_]_1

← MathLib Explorer

Lean4

@[tactic Mathlib.Tactic.Polyrith.«tacticPolyrithOnly[_]»]
public meta def «_aux_Mathlib_Tactic_Polyrith___elabRules_Mathlib_Tactic_Polyrith_tacticPolyrithOnly[_]_1» :
    Lean.Elab.Tactic.Tactic✝ := fun
  | `(tactic| polyrith$[ only]?$[ [$hyps,*]]?) => do
    throwError"`polyrith` is no longer available, \
              as the external service it relied on has been shut down."
  | _ => no_error_if_unused% throwUnsupportedSyntax✝

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

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

Разделы

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

Аффилиация

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