Jon Sterling on Nostr: The only annoying thing is that it does require one instance of weakening, which is ...
The only annoying thing is that it does require one instance of weakening, which is usually avoided in elaboration algorithms. Weakening in NbE is implemented by an eval-quote roundtrip; luckily, I have arranged for eval-quote to be very cheap because I do not eagerly unfold anything nor do I eta expand anything (so the process is type-free).
Published at
2025-02-22 21:58:43Event JSON
{
"id": "bc2a0facf7270b3c402541d7277ee3612debd1f47f962c302b18531916547101",
"pubkey": "ba51d3bb7fc92891016b5873c0b4f7c6a0550c964ec565ece24b6fc2dcf93301",
"created_at": 1740261523,
"kind": 1,
"tags": [
[
"e",
"163dcc32f5741c4a8bf758f554c995342eb5b2e4dbf51308e8e58a4efe13b38f",
"wss://relay.mostr.pub",
"reply"
],
[
"proxy",
"https://mathstodon.xyz/users/jonmsterling/statuses/114049779191740809",
"activitypub"
]
],
"content": "The only annoying thing is that it does require one instance of weakening, which is usually avoided in elaboration algorithms. Weakening in NbE is implemented by an eval-quote roundtrip; luckily, I have arranged for eval-quote to be very cheap because I do not eagerly unfold anything nor do I eta expand anything (so the process is type-free).",
"sig": "c5d1c4bfd079fe367d52efee41e6c103a20bb9906b1ad85a8438e7e3bac59a5f12e341d62e67104b9efec4c858ccb2844d18a4051e3d1a047670cecdadebb1e0"
}
