doc: Add description for `CompactCoreState`

2025-07-13 17:12:24 -07:00 · 2025-07-13 17:12:24 -07:00 · b101806c92
parent e58becd14a
commit b101806c92
1 changed files with 1 additions and 1 deletions
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@ -101,7 +101,7 @@ def environmentUnpickle (path : System.FilePath) (background? : Option Environme
  return (← resurrectEnvironment distilled background?, region)


-open Lean.Core in
+/-- `CoreM`'s state, with information irrelevant to pickling masked out -/
 structure CompactCoreState where
  -- env             : Environment
  nextMacroScope  : MacroScope     := firstFrontendMacroScope + 1