parseLRAT

Mathlib.Tactic.Sat.FromLRAT

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Sat.Parser.parseLRAT

Lean4

/-- Parse an LRAT file into a list of steps. -/
def parseLRAT : String.Parser (Array LRATStep) :=
  many do
    let step ← parseNat <* ws
    if (← peek!) = 'd' then
      skip <* ws;
      pure <| LRATStep.del (← parseNats)
    else
      ws;
      pure <| LRATStep.add step (← parseInts) (← parseInts)

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

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

Разделы

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

Аффилиация

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