Having a bit of fun re-implementing a normalisation-by-evaluation base elaborator using arena allocation for terms. Seems to work well, and doesn't result in much weirdness with lifetimes! Only end up needing to use reference counting in values.
Conversation
Looking forward to reading and learning from this!
1
Replying to
It's an draft PR here: github.com/yeslogic/fatho
Was running into walls with my current impl of Fathom so I've been trying to simplify stuff so that I can rethink my architectural approach.

