nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyzf5l64n2xk9azdrt6c96nwshexx45v4sduj7cyakmw005afuu05jm4rrqe (nprofile…rrqe) Yeah, I generally work in a 4 type setup:
term syntax
type syntax
term value
type value
So it seems like your proposal is the second of my two options, where I extend term syntax to be "the syntax of perhaps-not-fully-substituted term judgments" and analogous for the rest.
Just to make it clear what I mean by this, if I have
```
def f (x : Int) (y : Int) : Int = x + y
```
and I don't have pi types, then `f x` would be a "perhaps-not-fully substituted term judgment". Is there a better word for that?
Owen Lynch
npub1cj…fxs07
2025-12-28 20:40:22 UTC
in reply to nevent1q…jpy8
Author Public Key
npub1cjyyl7y66997ewku92pzvvhkyec43k7cde44rhgayxdwwl63axdqafxs07Seen on
wss://relay.ditto.pubPublished at
2025-12-28 20:40:22 UTCEvent JSON
{
"id": "212ef863f3aac32553d29cf7ce8caa3bba286d6443a7f802631242ff53ae747a",
"pubkey": "c4884ff89ad14becbadc2a822632f6267158dbd86e6b51dd1d219ae77f51e99a",
"created_at": 1766954422,
"kind": 1,
"tags": [
[
"p",
"934feab351ac5e89a35eb05d4dd0be4c6ad19583792f609db6dcf7d3a9e71f49",
"wss://relay.ditto.pub/"
],
[
"p",
"ba51d3bb7fc92891016b5873c0b4f7c6a0550c964ec565ece24b6fc2dcf93301",
"wss://relay.ditto.pub/"
],
[
"e",
"0ce6a94bca20250480f6404936810394d9d02ae2daa033cdb1f9ee37c4a50cf8",
"wss://relay.ditto.pub/",
"reply"
],
[
"proxy",
"https://mathstodon.xyz/users/olynch/statuses/115799125010738402",
"activitypub"
],
[
"client",
"Mostr",
"31990:6be38f8c63df7dbf84db7ec4a6e6fbbd8d19dca3b980efad18585c46f04b26f9:mostr",
"wss://relay.ditto.pub/"
]
],
"content": "nostr:nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyzf5l64n2xk9azdrt6c96nwshexx45v4sduj7cyakmw005afuu05jm4rrqe Yeah, I generally work in a 4 type setup:\n\nterm syntax\ntype syntax\nterm value\ntype value\n\nSo it seems like your proposal is the second of my two options, where I extend term syntax to be \"the syntax of perhaps-not-fully-substituted term judgments\" and analogous for the rest.\n\nJust to make it clear what I mean by this, if I have\n\n```\ndef f (x : Int) (y : Int) : Int = x + y\n```\n\nand I don't have pi types, then `f x` would be a \"perhaps-not-fully substituted term judgment\". Is there a better word for that?",
"sig": "c661816c3c9e2f60386fb5b7df50f27d50d8ac8e28c424a29b3998ce1e67916b761aa08a99aa2eb02742aa0c3105759e75c41d780670e864efddb1579cd48354"
}