nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyzf5l64n2xk9azdrt6c96nwshexx45v4sduj7cyakmw005afuu05jm4rrqe (nprofile…rrqe) These are all good points.
I think the real question for me is how this effects my term/type *syntax*. E.g. now that (concrete syntax identifiers) can refer either to an element of a type or a proper judgment, should I have two mutually recursive syntax trees that I elaborate into or just one? And should syn/chk return a sum type between them?
Perhaps they really should be distinguished in the concrete syntax for clarity...
Owen Lynch
npub1cj…fxs07
2025-12-29 19:08:39 UTC
in reply to nevent1q…w400
Author Public Key
npub1cjyyl7y66997ewku92pzvvhkyec43k7cde44rhgayxdwwl63axdqafxs07Seen on
wss://relay.ditto.pubPublished at
2025-12-29 19:08:39 UTCEvent JSON
{
"id": "426b42bb5b5e7d08d1fb20f5a9619deb313df1f74ee788c398ef1216d799cb16",
"pubkey": "c4884ff89ad14becbadc2a822632f6267158dbd86e6b51dd1d219ae77f51e99a",
"created_at": 1767035319,
"kind": 1,
"tags": [
[
"p",
"934feab351ac5e89a35eb05d4dd0be4c6ad19583792f609db6dcf7d3a9e71f49",
"wss://relay.ditto.pub/"
],
[
"p",
"ba51d3bb7fc92891016b5873c0b4f7c6a0550c964ec565ece24b6fc2dcf93301",
"wss://relay.ditto.pub/"
],
[
"e",
"f0e0b89b4666e81e7b45316877167bc0ebc161b256e82ddccb2b5433d3946d5b",
"wss://relay.ditto.pub/",
"reply"
],
[
"proxy",
"https://mathstodon.xyz/users/olynch/statuses/115804426698210139",
"activitypub"
],
[
"client",
"Mostr",
"31990:6be38f8c63df7dbf84db7ec4a6e6fbbd8d19dca3b980efad18585c46f04b26f9:mostr",
"wss://relay.ditto.pub/"
]
],
"content": "nostr:nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyzf5l64n2xk9azdrt6c96nwshexx45v4sduj7cyakmw005afuu05jm4rrqe These are all good points.\n\nI think the real question for me is how this effects my term/type *syntax*. E.g. now that (concrete syntax identifiers) can refer either to an element of a type or a proper judgment, should I have two mutually recursive syntax trees that I elaborate into or just one? And should syn/chk return a sum type between them? \n\nPerhaps they really should be distinguished in the concrete syntax for clarity...",
"sig": "9c7acdc61dd5a6ccedae798a229e2d5205b64522aa887ec6f4d42561bba99b1f984bea225343b4e8f214fc555a35858c8ce2b0aaf6ab3a67f2dbecdcf055fb43"
}