Jon Sterling on Nostr: nprofile1q…ulpgt Yeah... When working in Lean, I use intrinsically typed de bruijn ...

nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpq26zlh0z0afh055uppfrtzhkkr824ya2p9wa3a2ghhj8ntfpnm7xqtulpgt (nprofile…lpgt) Yeah... When working in Lean, I use intrinsically typed de bruijn indices; but for the de bruijn level layer, I don't really know how or if it is possible to gain benefits from benefit types here (because you want weakening to be silent and not require a traversal). A good representation of the latter would be really cool, but I am not sure what it would be :)