Are there any connections between Klister-style stuck macros and neutral terms in NBE? Superficially they seem similar, both being mechanisms to pause further work; with stuck macros, you don't have enought type info, with neutral terms you don't have a value in the environment.
Conversation
This recorded talk does mention "inspired by dependent types" so maybe that's all there is to it.
davidchristiansen.dk/pubs/tyde2020-
2
Replying to