inductive Ion.SymbolTableEntry : Type

• string (s : String) : SymbolTableEntry
• record (name : Lean.Name) : SymbolTableEntry

@[implicit_reducible]

instance Ion.instDecidableEqSymbolTableEntry : DecidableEq SymbolTableEntry

Equations

• Ion.instDecidableEqSymbolTableEntry = Ion.instDecidableEqSymbolTableEntry.decEq

def Ion.instDecidableEqSymbolTableEntry.decEq (x✝ x✝¹ : SymbolTableEntry) : Decidable (x✝ = x✝¹)

Equations

• Ion.instDecidableEqSymbolTableEntry.decEq (Ion.SymbolTableEntry.string a) (Ion.SymbolTableEntry.string b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Ion.instDecidableEqSymbolTableEntry.decEq (Ion.SymbolTableEntry.string s) (Ion.SymbolTableEntry.record name) = isFalse ⋯
• Ion.instDecidableEqSymbolTableEntry.decEq (Ion.SymbolTableEntry.record name) (Ion.SymbolTableEntry.string s) = isFalse ⋯
• Ion.instDecidableEqSymbolTableEntry.decEq (Ion.SymbolTableEntry.record a) (Ion.SymbolTableEntry.record b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Ion.instHashableSymbolTableEntry : Hashable SymbolTableEntry

Equations

• Ion.instHashableSymbolTableEntry = { hash := Ion.instHashableSymbolTableEntry.hash }

def Ion.instHashableSymbolTableEntry.hash : SymbolTableEntry → UInt64

Equations

• Ion.instHashableSymbolTableEntry.hash (Ion.SymbolTableEntry.string a) = mixHash 0 (hash a)
• Ion.instHashableSymbolTableEntry.hash (Ion.SymbolTableEntry.record a) = mixHash 1 (hash a)

def Ion.instReprSymbolTableEntry.repr : SymbolTableEntry → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Ion.instReprSymbolTableEntry : Repr SymbolTableEntry

Equations

• Ion.instReprSymbolTableEntry = { reprPrec := Ion.instReprSymbolTableEntry.repr }

@[implicit_reducible]

instance Ion.instToExprSymbolTableEntry : Lean.ToExpr SymbolTableEntry

Equations

• Ion.instToExprSymbolTableEntry = { toExpr := Ion.instToExprSymbolTableEntry._private_1, toTypeExpr := Ion.instToExprSymbolTableEntry._private_3 }

structure Ion.NameSymbols : Type

• name : Lean.Name
• entries : Array SymbolTableEntry

structure Ion.SymbolTableEntries : Type

• array : Array SymbolTableEntry
• names : Std.HashMap SymbolTableEntry Nat

structure Ion.IonTypeState : Type

• map₁ : Std.HashMap Lean.Name (Array SymbolTableEntry)
• map₂ : Lean.PHashMap Lean.Name SymbolTableEntries
• scope : Option (Lean.Name × Lean.Expr)

@[implicit_reducible]

instance Ion.instInhabitedIonTypeState : Inhabited IonTypeState

Equations

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

def Ion.instInhabitedIonTypeState.default : IonTypeState

Equations

• Ion.instInhabitedIonTypeState.default = { map₁ := default, map₂ := default, scope := default }

def Ion.IonTypeState.getEntries? (s : IonTypeState) (name : Lean.Name) : Option (Array SymbolTableEntry)

Equations

• s.getEntries? name = match Lean.PersistentHashMap.find? s.map₂ name with | some e => some e.array | none => s.map₁[name]?

def Ion.IonTypeState.getEntries (s : IonTypeState) (name : Lean.Name) : Array SymbolTableEntry

Equations

• s.getEntries name = match Lean.PersistentHashMap.find? s.map₂ name with | some e => e.array | none => s.map₁.getD name #[]

def Ion.IonTypeState.getIndexOf (s : IonTypeState) (name : Lean.Name) (entry : SymbolTableEntry) : Nat

Equations

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

def Ion.IonTypeState.addEntry (s : IonTypeState) (name : Lean.Name) (entry : SymbolTableEntry) : IonTypeState

Equations

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

opaque Ion.ionDialectExt : Lean.PersistentEnvExtension NameSymbols NameSymbols IonTypeState