line!

Mathlib.Tactic.Explode.Datatypes

URI: https://scilib.ai/kg/mathlib#Mathlib.Explode.Entry.line!

Lean4

/-- Get the `line` for an `Entry` that has been added to the `Entries` structure. -/
def line! (entry : Entry) : Nat :=
  entry.line.get!

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

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

Разделы

Аффилиация

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