import Lean
-- import Batteries.Util.TermUnsafe

open Lean Meta Elab Command Tactic

abbrev 
Entry: Type
Entry := 
String: Type
String
abbrev 
EntryList: Type
EntryList := 
List: Type → Type
List 
Entry: Type
Entry

-- Lean server printed an error: libc++abi: terminating due to uncaught exception of type lean::exception: cannot evaluate `[init]` declaration 'proofStatesExt' in the same module

initialize 
myExt: SimplePersistentEnvExtension Entry EntryList
myExt : 
SimplePersistentEnvExtension: Type → Type → Type
SimplePersistentEnvExtension 
Entry: Type
Entry 
EntryList: Type
EntryList ←
  
registerSimplePersistentEnvExtension: {α σ : Type} → [inst : Inhabited σ] → SimplePersistentEnvExtensionDescr α σ → IO (SimplePersistentEnvExtension α σ)
registerSimplePersistentEnvExtension {
    addEntryFn := (·.
concat: {α : Type} → List α → α → List α
concat)
    addImportedFn := 
mkStateFromImportedEntries: {α σ : Type} → (σ → α → σ) → σ → Array (Array α) → σ
mkStateFromImportedEntries (·.
concat: {α : Type} → List α → α → List α
concat) 
{}: EntryList
{}
  }

elab (name := 
Proof: ParserDescr
Proof) "Proof" 
_desc: TSyntaxArray Name.anonymous
_desc:
interpolatedStr: Parser.Parser → Parser.Parser
interpolatedStr(
term: Parser.Category
term)* ":" 
_t: TSyntax `Lean.Parser.Tactic.tacticSeq
_t:
tacticSeq: Parser.Parser
tacticSeq : 
tactic: Parser.Category
tactic => do
  unsafe 
enableInitializersExecution: IO Unit
enableInitializersExecution

  
modifyEnv: {m : Type → Type} → [self : MonadEnv m] → (Environment → Environment) → m Unit
modifyEnv fun 
env: Environment
env =>
    
myExt: SimplePersistentEnvExtension Entry EntryList
myExt.
addEntry: {α β σ : Type} → PersistentEnvExtension α β σ → Environment → β → Environment
addEntry 
env: Environment
env 
"": String
""