nprofile1q…fw8t5 nprofile1q…4rrqe Actually, it is MLTT! See, like, §4.1.3 in ...

Why Nostr? What is Njump? Join Nostr

Amélia Liao 🍊😈

npub105…yvwnw

2025-12-20 12:36:42 UTC

in reply to nevent1q…fdpt

nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyry2ysn5av9pr8m76kgpggcflz294t0pr9shd99kh8redys7ku0xkefw8t5 (nprofile…w8t5) nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyzf5l64n2xk9azdrt6c96nwshexx45v4sduj7cyakmw005afuu05jm4rrqe (nprofile…rrqe) Actually, it is MLTT! See, like, §4.1.3 in Jesper's thesis. It shows how to automatically construct an equivalence between true ≡ true and ⊤, without K, and then §4.3 shows you how to deploy that equivalence to translate the pattern-matching function you wrote to one in terms of nothing but eliminators while preserving all the clauses you wrote as definitional computation rules. There is no bug here. There's barely even a feature request here, since you've already lobbied for --no-pattern-matching in the past. I don't want to commit to supporting twelve other feature flags for whatever unification step you feel unhappy with on a given day. You know these functions all rely on the exact same behaviour, right? Why isn't this file called MLTT.Wrong-Vector?

Author Public Key

npub105djthvncz3tms6ke37w4579d0qqmf2e6xt9p7z5h3ayq0wtq7pswyvwnw

Seen on

wss://relay.ditto.pub

Show more details

Published at

2025-12-20 12:36:42 UTC

Kind type

1 Short Text Note

Event JSON

{ "id": "e74aac03a086be7fe18aba03030b697975a463d16310386236192e9f565e513a", "pubkey": "7d1b25dd93c0a2bdc356cc7cead3c56bc00da559d19650f854bc7a403dcb0783", "created_at": 1766234202, "kind": 1, "tags": [ [ "p", "c8a24274eb0a119f7ed590142309f8945aade119617694b6b9c796921eb71e6b", "wss://relay.ditto.pub/" ], [ "p", "934feab351ac5e89a35eb05d4dd0be4c6ad19583792f609db6dcf7d3a9e71f49", "wss://relay.ditto.pub/" ], [ "p", "5c675fe7561c52f2c0ea8db391d2c3a46556bec9a3c0a4b4f10f234fe03f58ca", "wss://relay.ditto.pub/" ], [ "p", "ba51d3bb7fc92891016b5873c0b4f7c6a0550c964ec565ece24b6fc2dcf93301", "wss://relay.ditto.pub/" ], [ "e", "388286df9f4907ab610f12856c32961fb985df006035732c25d63da6066f8ef8", "wss://relay.ditto.pub/", "reply" ], [ "proxy", "https://types.pl/users/amy/statuses/115751924695010000", "activitypub" ], [ "client", "Mostr", "31990:6be38f8c63df7dbf84db7ec4a6e6fbbd8d19dca3b980efad18585c46f04b26f9:mostr", "wss://relay.ditto.pub/" ] ], "content": "nostr:nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyry2ysn5av9pr8m76kgpggcflz294t0pr9shd99kh8redys7ku0xkefw8t5 nostr:nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyzf5l64n2xk9azdrt6c96nwshexx45v4sduj7cyakmw005afuu05jm4rrqe Actually, it is MLTT! See, like, §4.1.3 in Jesper's thesis. It shows how to automatically construct an equivalence between true ≡ true and ⊤, without K, and then §4.3 shows you how to deploy that equivalence to translate the pattern-matching function you wrote to one in terms of nothing but eliminators while preserving all the clauses you wrote as definitional computation rules. There is no bug here. There's barely even a feature request here, since you've already lobbied for --no-pattern-matching in the past. I don't want to commit to supporting twelve other feature flags for whatever unification step you feel unhappy with on a given day. You know these functions all rely on the exact same behaviour, right? Why isn't this file called MLTT.Wrong-Vector?", "sig": "52eb8055a445386a532d57f3b8ed72f72f5bb185d0aad4d4519ae72daa71b27adb0b74cf98fb2e1421ef0f4c69b424e805ba8cf66918394688e37a4c094da43b" }