- map : Std.HashMap String Ion.SymbolId
Instances For
@[implicit_reducible]
Equations
Equations
Instances For
Equations
- tbl.size = (Ion.SymbolTable.array✝ tbl).size
Instances For
@[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.
Lookup symbol and return SymbolId.zero if not defined.
Equations
- Ion.SymbolTable.symbolId sym tbl = (Ion.SymbolTable.map✝ tbl).getD sym Ion.SymbolId.zero
Instances For
Intern a string into a symbol.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Minimal system symbol table.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Ion.SymbolTable.ofLocals locals = Array.foldl (fun (tbl : Ion.SymbolTable) (sym : String) => (Ion.SymbolTable.intern sym tbl).snd) Ion.SymbolTable.system locals
Instances For
@[implicit_reducible]
Equations
- Ion.SymbolTable.instQuoteMkStr1 = { quote := fun (st : Ion.SymbolTable) => Lean.Syntax.mkCApp `Ion.SymbolTable.ofLocals #[Lean.quote `term st.locals] }