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
Implicit/explicit subst in formalization is up to taste IMO, implicit subst would have worked in nbe-martinlof as well. In Coq I would choose implicit subst because of autosubst. In practical implementation, implicit subst is better, or more precisely ...
1
1
... we streamline explicit subst in practical implementation so that it only appears in closures (where it's actually needed).
1
1
Replying to
Thanks for answering!
Ohhh right. Forgot that closures fulfilled the role of the explicit substs. Still feels kinda ick that there is still such a big gap between implementation and proof, but perhaps that will be fixed in time... 🤔