instOrdEntry

Mathlib.Tactic.TacticAnalysis

URI: https://scilib.ai/kg/mathlib#Mathlib.TacticAnalysis.instOrdEntry

Lean4

instance : Ord Entry where compare a b := (@lexOrd _ _ ⟨Lean.Name.cmp⟩ ⟨Lean.Name.cmp⟩).compare (a.1, a.2) (b.1, b.2)

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

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

Разделы

Аффилиация

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