evalLazyEntry

Mathlib.Lean.Meta.RefinedDiscrTree.Encode

URI: https://scilib.ai/kg/mathlib#Lean.Meta.RefinedDiscrTree.evalLazyEntry

Lean4

/-- A single step in evaluating a `LazyEntry`. Allow multiple different outcomes. -/
def evalLazyEntry (entry : LazyEntry) (eta : Bool) : MetaM (Option (List (Key × LazyEntry))) := do
  if let key :: computedKeys := entry.computedKeys then
      -- If there is already a result available, use it.

    return some [(key, { entry with computedKeys })]
  else
    withMCtx entry.mctx do
        let entry ← processPrevious entry
        evalLazyEntryAux entry eta

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

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

Разделы

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

Аффилиация

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