hey hey! Just wondering what you think of bitbucket.org/pl-uwr/nbe-mar - been curious of approaches to nbe that might be formalizable, but concerned this might end up slowing things down. Eg. not sure how the explicit substs would fare - increasing pointer indirection?
Conversation
Also wondering if you plan on doing pattern matching compilation during the elaboration phase at stage in smalltt - atm I’m trying to add it in my port of nbe-for-mltt, but it seems quite tricky to do after name resolution has been done - have to handle db indices+pattern indices
Replying to
Curious if has any thoughts on how to tackle pattern elaboration in a lang like nbe-for-mltt/mini-tt too. Come across any other examples I might be able to steal from? 😅
1