isOutside

Mathlib.Tactic.Linter.CommandStart

URI: https://scilib.ai/kg/mathlib#Mathlib.Linter.Style.CommandStart.isOutside

Lean4

/-- Given a `HashSet` of `String.Range`s `rgs` and a further `String.Range` `rg`,
`isOutside rgs rg` returns `false` if and only if `rgs` contains a range that completely contains
`rg`.

The linter uses this to figure out which nodes should be ignored.
-/
def isOutside (rgs : Std.HashSet String.Range) (rg : String.Range) : Bool :=
  rgs.all fun { start := a, stop := b } ↦ !(a ≤ rg.start && rg.stop ≤ b)

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

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

Разделы

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

Аффилиация

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