structure StrataDDM.PersistentDialect : Type

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

def StrataDDM.PersistentDialect.ofDialect (leanName : Lean.Name) (d : Dialect) : PersistentDialect

Equations

• StrataDDM.PersistentDialect.ofDialect leanName d = { leanName := leanName, name := d.name, imports := d.imports, declarations := d.declarations, typecheck := d.typecheck }

def StrataDDM.PersistentDialect.dialect (pd : PersistentDialect) : Dialect

Equations

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

structure StrataDDM.DialectState : Type

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

@[implicit_reducible]

instance StrataDDM.instInhabitedDialectState : Inhabited DialectState

Equations

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

def StrataDDM.instInhabitedDialectState.default : DialectState

Equations

• StrataDDM.instInhabitedDialectState.default = { loaded := default, nameMap := default, newDialects := 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