discreteCases

Mathlib.CategoryTheory.Discrete.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Discrete.discreteCases

Lean4

/-- Use:
```
attribute [local aesop safe tactic (rule_sets := [CategoryTheory])]
  CategoryTheory.Discrete.discreteCases
```
to locally gives `cat_disch` the ability to call `cases` on
`Discrete` and `(_ : Discrete _) ⟶ (_ : Discrete _)` hypotheses.
-/
def discreteCases : TacticM Unit := do
  evalTactic
      (← `(tactic| discrete_cases))
        -- TODO: investigate turning on either
        -- `attribute [aesop safe cases (rule_sets := [CategoryTheory])] Discrete`
        -- or
        -- `attribute [aesop safe tactic (rule_sets := [CategoryTheory])] discreteCases`
        -- globally.

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

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

Разделы

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

Аффилиация

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