class StrataDDM.HasInputContext (m : Type → Type u_1) [Functor m] : Type u_1

• getInputContext : m Parser.InputContext
• getFileName : m System.FilePath

def StrataDDM.instToExprSourcedProgram.toExpr : SourcedProgram → Lean.Expr

Equations

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

@[instance_reducible]

instance StrataDDM.instToExprSourcedProgram : Lean.ToExpr SourcedProgram

Equations

• StrataDDM.instToExprSourcedProgram = { toExpr := StrataDDM.instToExprSourcedProgram.toExpr, toTypeExpr := Lean.Expr.const `StrataDDM.SourcedProgram [] }

@[instance_reducible]

instance StrataDDM.instHasInputContextCommandElabM : HasInputContext Lean.Elab.Command.CommandElabM

Equations

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

@[instance_reducible]

instance StrataDDM.instHasInputContextCoreM : HasInputContext Lean.CoreM

Equations

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

def StrataDDM.addDefn (name : Lean.Name) (type value : Lean.Expr) (levelParams : List Lean.Name := []) (hints : Lean.ReducibilityHints := Lean.ReducibilityHints.abbrev) (safety : Lean.DefinitionSafety := Lean.DefinitionSafety.safe) (all : List Lean.Name := [name]) (isMeta : Bool := false) : Lean.CoreM Unit

Add a definition to environment and compile it.

Equations

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

def StrataDDM.declareDialect (d : Dialect) : Lean.Elab.Command.CommandElabM Unit

Declare dialect and add to environment.

Equations

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

def StrataDDM.strataDialectCommand : Parser.Parser

Equations

• StrataDDM.strataDialectCommand = StrataDDM.ExternParser.mkParser `strataDialectCommand "#dialect" "#end"

def StrataDDM.strataDialectImpl : Lean.Elab.Command.CommandElab

Equations

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

def StrataDDM.strataProgram : Parser.Parser

Equations

• StrataDDM.strataProgram = StrataDDM.ExternParser.mkParser `strataProgram "#strata" "#end"

def StrataDDM.strataProgramImpl : Lean.Elab.Term.TermElab

Equations

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

def StrataDDM.loadDialectCommand : Lean.ParserDescr

Equations

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

def StrataDDM.getModuleRoot (path : System.FilePath) (modName : Lean.Name) : Except String System.FilePath

Derive the package source root from a module's file path and name by stripping one directory component per name part. For example, given /repo/Strata/Languages/Foo.lean and module name Strata.Languages.Foo, returns /repo.

Equations

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

def StrataDDM.loadDialectImpl : Lean.Elab.Command.CommandElab

Equations

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