jnkrtech on Nostr: nprofile1q…d6kk0 nprofile1q…ulpgt If I might ask one more question, I notice that ...

nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpqjd874v63430gng67kpw5m597f34dr9vr0yhkp8dkmnma8208raysyd6kk0 (nprofile…6kk0) nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpq26zlh0z0afh055uppfrtzhkkr824ya2p9wa3a2ghhj8ntfpnm7xqtulpgt (nprofile…lpgt) If I might ask one more question, I notice that in your Tm type you only store the index, not the type (in the object language sense) of the term. Is that to simplify the example? I’m not clear on whether my life will be easier if I try to store the typing context as a separate lookup table or if I stick the types of my terms directly into the definition of the terms themselves.