Paul Stansifer

> But there's nothing to call "body"; the `Star` could potentially contain, say, three `Named` nodes. What do we do then? I think this isn't a big deal. Let's try...

Wait, this is actually a big deal. Currently, "dotdotdot" is, grammatically, a `Scope` whose grammar contains a bunch of complexity, including other `Scope`s it doesn't need to peek inside (which...

Ideas: * Some new kind of pre-match, but in positive modes this time (note: nooo, we want to get rid of pre-match, somehow). * When rewriting form grammars, also replace...

Okay, I think that resolving `...[ ]...` at `'[ ]'`-time should work. The quasiquotation means that all bindings are shifted by a phase, so the dotdotdots it contains (operating, as...

Oh, however we do this, this is going to expose a soundness problem (actually, it's already been visible): when we typecheck a repetition of unknown length, we just treat it...

Maybe we can do some ad-hoc gensymming in a way that makes this work more cleanly everywhere else. We find-and-replace all `Star`es/`Plus`es with an import from an adjacent `dotdotdot` form...

Okay, I tried adding a repetition form to `Ast`, and I gotta say, `alpha.rs` doesn't like having an intrusion on the middle of its `EnvMBE`s. I think it could be...

Oops, didn't mean to close this.

Okay, this rabbit hole is deep. I'm partway through rewriting `EnvMBE` (#45), and it's, uh, not as simple as I expected. I still think that `EnvMBE` should be rewritten (I...

Exported names aren't the product of arbitrary computation; they use betas too! But this should be easy to solve: we just introduce a new type form (`Unrepeat`?) that generates the...