structure StrataDDM.PersistentDialect : Type

• leanName : Lean.Name
• name : DialectName
• imports : Array DialectName
• declarations : Array Decl

structure StrataDDM.DialectState : Type

• loaded : Elab.LoadedDialects
• nameMap : Std.HashMap DialectName Lean.Name
• newDialects : Array (Lean.Name × Dialect)

def StrataDDM.instInhabitedDialectState.default : DialectState

Equations

• StrataDDM.instInhabitedDialectState.default = { loaded := default, nameMap := default, newDialects := default }

@[implicit_reducible]

instance StrataDDM.instInhabitedDialectState : Inhabited DialectState

Equations

• StrataDDM.instInhabitedDialectState = { default := StrataDDM.instInhabitedDialectState.default }

def StrataDDM.DialectState.addDialect! (s : DialectState) (d : Dialect) (name : Lean.Name) (isNew : Bool) : DialectState

Equations

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

opaque StrataDDM.dialectExt : Lean.PersistentEnvExtension PersistentDialect (Lean.Name × Dialect) DialectState