structure Ion.SymbolIdCache : Type

Stores tables used to efficiently serialize values.

• globalCache : Array Nat

  Global array for entries

• offset : Nat

  Offset into global array for this type.

def Ion.SymbolIdCache.id! (ctx : String) (refs : SymbolIdCache) (i : Nat) : SymbolId

Equations

• One or more equations did not get rendered due to their size.

def Ion.SymbolIdCache.ref! (refs : SymbolIdCache) (tp : String) (i : Nat) : SymbolIdCache

Returns the symbol id cache for the given type and index.

Equations

• One or more equations did not get rendered due to their size.

structure Ion.LeanSymbolTableMap : Type

• symtab : SymbolTable
• nameMap : Std.HashMap Lean.Name Nat
• entries : Array Nat

def Ion.instInhabitedLeanSymbolTableMap.default : LeanSymbolTableMap

Equations

• Ion.instInhabitedLeanSymbolTableMap.default = { symtab := default, nameMap := default, entries := default }

@[implicit_reducible]

instance Ion.instInhabitedLeanSymbolTableMap : Inhabited LeanSymbolTableMap

Equations

• Ion.instInhabitedLeanSymbolTableMap = { default := Ion.instInhabitedLeanSymbolTableMap.default }

def Ion.LeanSymbolTableMap.addEntry : SymbolTableEntry → StateM LeanSymbolTableMap Nat

Equations

• One or more equations did not get rendered due to their size.

def Ion.LeanSymbolTableMap.addRecord (tbl : LeanSymbolTableMap) (name : Lean.Name) (entries : Array SymbolTableEntry) : Nat × LeanSymbolTableMap

Equations

• One or more equations did not get rendered due to their size.

partial def Ion.LeanSymbolTableMap.addToSymbolTable (s : IonTypeState) (name : Lean.Name) : StateT LeanSymbolTableMap (Except String) Nat

class Ion.CachedToIon (α : Type u_1) : Type u_1

• cachedToIon : SymbolIdCache → α → InternM (Ion SymbolId)

@[implicit_reducible]

instance Ion.CachedToIon.instArray {α : Type u_1} [h : CachedToIon α] : CachedToIon (Array α)

Equations

• Ion.CachedToIon.instArray = { cachedToIon := fun (refs : Ion.SymbolIdCache) (a : Array α) => Ion.CachedToIon.instArray._private_1 refs a }

@[implicit_reducible]

instance Ion.CachedToIon.instList {α : Type u_1} [h : CachedToIon α] : CachedToIon (List α)

Equations

• Ion.CachedToIon.instList = { cachedToIon := fun (refs : Ion.SymbolIdCache) (a : List α) => Ion.CachedToIon.instList._private_1 refs a }

def Ion.declareIonScope : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Ion.declareIonScopeImpl : Lean.Elab.Term.TermElab

Equations

• One or more equations did not get rendered due to their size.

def Ion.declareIonSymbol : Lean.ParserDescr

Equations

• Ion.declareIonSymbol = Lean.ParserDescr.node `Ion.declareIonSymbol 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "ionSymbol!") (Lean.ParserDescr.const `str))

def Ion.declareIonSymbolImpl : Lean.Elab.Term.TermElab

Equations

• One or more equations did not get rendered due to their size.

def Ion.declareIonTypeOf : Lean.ParserDescr

Equations

• Ion.declareIonTypeOf = Lean.ParserDescr.node `Ion.declareIonTypeOf 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "ionTypeOf!") (Lean.ParserDescr.cat `term 0))

def Ion.declareIonTypeOfImpl : Lean.Elab.Term.TermElab

Equations

• One or more equations did not get rendered due to their size.

def Ion.declareIonRefEntry : Lean.ParserDescr

Equations

• Ion.declareIonRefEntry = Lean.ParserDescr.node `Ion.declareIonRefEntry 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "ionRefEntry!") (Lean.ParserDescr.cat `term 0))

unsafe def Ion.declareIonRefCacheImpl : Lean.Elab.Term.TermElab

Equations

• One or more equations did not get rendered due to their size.

def Ion.termIonRef!_ : Lean.ParserDescr

Equations

• Ion.termIonRef!_ = Lean.ParserDescr.node `Ion.termIonRef!_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "ionRef!") (Lean.ParserDescr.cat `term 0))

def Ion.getIonEntries : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Ion.getIonEntriesImpl : Lean.Elab.Term.TermElab

Equations

• One or more equations did not get rendered due to their size.

def Ion.declareIonSymbolTable : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Ion.declareIonSymbolTableImpl : Lean.Elab.Command.CommandElab

Equations

• One or more equations did not get rendered due to their size.