tacticFin_omega

Mathlib.Data.Fin.Basic

URI: https://scilib.ai/kg/mathlib#Fin.tacticFin_omega

Lean4

/-- Preprocessor for `omega` to handle inequalities in `Fin`.
Note that this involves a lot of case splitting, so may be slow.
-/
-- Further adjustment to the simp set can probably make this more powerful.
-- Please experiment and PR updates!

@[tactic_parser 1000]
public meta def tacticFin_omega : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Fin.tacticFin_omega 1024 (ParserDescr.nonReservedSymbol✝ "fin_omega" false✝)

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

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

Разделы

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

Аффилиация

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