Jon Sterling on Nostr: nprofile1q…tcpun nprofile1q…ulpgt When you spend a lot of time programming and ...

nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpqkyagcdfagmkfyqwplpv0neng7nq24p4q3l4v7jhe3srlsmntufzs8tcpun (nprofile…cpun) nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpq26zlh0z0afh055uppfrtzhkkr824ya2p9wa3a2ghhj8ntfpnm7xqtulpgt (nprofile…lpgt) When you spend a lot of time programming and proving in dependent type theory, you start to get an instinct that any time you see the same index twice in a type, you should forget that and try to write a generalised function where those indices are made different... Tricks of the trade... (This requires a healthy intolerance for "head bashing", so that you quickly switch to trying to find a way around it.)