is it possible to elaborate an entire module?

Stream: lean4

[Yuri]

All syntax and elaboration examples I see assume there is already a module. Could I elaborate a new command in module A that dynamically generates a module B, C etc? Or is there constraint is that all new definitions are elaborated into an existing module?

AFAIK, Alloy is triggered by lake to load the environment and generate .c and .h files outside of the Lean compiler. What I would like to do is use the Lean code generator to do the same but within the Lean compiler.

[Robert Maxton]

What do you mean by module? You can certainly have a syntax that expands into

namespace Foo

def Bar := ...

end Foo

or just

def Foo.Bar := ...

[Robert Maxton]

If you want a whole new file, then I don't know

[Yuri]

Yes, I meant a whole new file. I would like to explore importing other types of sources (in my case .h files) that generate types on the fly. A (module) type provider that produces virtual modules that only exist as compiled artifacts (located in .lake/build/ir.

For instance (hand waving a few specific challenges):

import MyDuckDB.Types from "./includes/duckdb.h"