Documentation

StrataDDM.AST.Lemmas

source
@[simp]
theorem StrataDDM.Program.create_dialects (d : DialectMap) (dn : DialectName) (cmds : Array Operation) :
(create d dn cmds).dialects = d
source
@[simp]
theorem StrataDDM.Program.create_dialect (d : DialectMap) (dn : DialectName) (cmds : Array Operation) :
(create d dn cmds).dialect = dn
source
@[simp]
theorem StrataDDM.Program.create_commands (d : DialectMap) (dn : DialectName) (cmds : Array Operation) :
(create d dn cmds).commands = cmds