ROccs

Mathlib.Tactic.CC.Datatypes

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.CC.ACEntry.ROccs

Lean4

/-- Returns the occurrences of this entry in either the LHS or RHS. -/
def ROccs (ent : ACEntry) : (inLHS : Bool) → ACAppsSet
  | true => ent.RLHSOccs
  | false => ent.RRHSOccs

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

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

Разделы

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

Аффилиация

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