structure Ion.SymbolTable : Type

• array : Array String
• map : Std.HashMap String Ion.SymbolId
• locals : Array String

@[implicit_reducible]

instance Ion.instInhabitedSymbolTable : Inhabited SymbolTable

Equations

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

def Ion.instInhabitedSymbolTable.default : SymbolTable

Equations

• Ion.instInhabitedSymbolTable.default = { array := default, map := default, locals := default }

def Ion.SymbolTable.size (tbl : SymbolTable) : Nat

Equations

• tbl.size = (Ion.SymbolTable.array✝ tbl).size

@[implicit_reducible]

instance Ion.SymbolTable.instGetElem?SymbolIdStringLtNatValueSize : GetElem? SymbolTable SymbolId String fun (tbl : SymbolTable) (idx : SymbolId) => idx.value < tbl.size

Equations

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

def Ion.SymbolTable.symbolId (sym : String) (tbl : SymbolTable) : SymbolId

Lookup symbol and return SymbolId.zero if not defined.

Equations

• Ion.SymbolTable.symbolId sym tbl = (Ion.SymbolTable.map✝ tbl).getD sym Ion.SymbolId.zero

def Ion.SymbolTable.intern (sym : String) (tbl : SymbolTable) : SymbolId × SymbolTable

Intern a string into a symbol.

Equations

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

def Ion.SymbolTable.ionSharedSymbolTableEntries : Array String

Equations

• Ion.SymbolTable.ionSharedSymbolTableEntries = #["$ion", "$ion_1_0", "$ion_symbol_table", "name", "version", "imports", "symbols", "max_id", "$ion_shared_symbol_table"]

def Ion.SymbolTable.system : SymbolTable

Minimal system symbol table.

Equations

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

def Ion.SymbolTable.ofLocals (locals : Array String) : SymbolTable

Equations

• Ion.SymbolTable.ofLocals locals = Array.foldl (fun (tbl : Ion.SymbolTable) (sym : String) => (Ion.SymbolTable.intern sym tbl).snd) Ion.SymbolTable.system locals

@[implicit_reducible]

instance Ion.SymbolTable.instQuoteMkStr1 : Lean.Quote SymbolTable

Equations

• Ion.SymbolTable.instQuoteMkStr1 = { quote := fun (st : Ion.SymbolTable) => Lean.Syntax.mkCApp `Ion.SymbolTable.ofLocals #[Lean.quote `term st.locals] }