I was thinking about how to support multiple files and one approach might be to make it possible to take an lexp and print it to a file, and then read it back. Then "exporting" the definitions of a particular module could look something like "take those defs, put them into a tuple, and print it to the file", and then importing definitions from a file would be a macro which reads the file and returns the corresponding lexp. As for how to "print & read", there'd be two ways to go about it: A- define brand new primitives that go straight from lexp <-> string. B- rework our lexp <-> sexp code to make it robust enough. Option B would also be useful in macros, so it's definitely something we should try to do. But it also means that reading would go through "sexp -> lexp" i.e. through elaboration. We could probably arrange for it not to do any macro-expansion and maybe also to avoid any need for unification, but it seems like it'd inherently be clunky/inefficient. So, I think option A is preferable. Stefan