nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyrj7vmtena97hded0cqwgs6heq8ddx9dc2kvd8vch7q9mgvdj3z67jx00p2 (nprofile…00p2) Hopefully I was not too far off base, though I floundered at conveying what was going on with ACL2 functions needing to be total, and what that meant viz guards (and using acl2 primitives like zp for their guards).
Thanks for providing the dates, actual university and such live, I think I said 1980 when I meant 1990 which you corrected.
I was pleasantly surprised by Ramin Honary (nprofile…w3ml) 's topics on the day I had been planning to miss but I was not prepared to opine on ACL2.
screwlisp
npub13r…sa54f
2025-11-26 02:22:28 UTC
in reply to nevent1q…xgxt
Author Public Key
npub13rtszkjs767qk5rruzx5ggcf8jqgvtyr7xq88lfg0lxth6rnyjkqmsa54fSeen on
wss://relay.mostr.pubPublished at
2025-11-26 02:22:28 UTCEvent JSON
{
"id": "717ab03e6ea9fbc7d18a576a407bf53acdc5d229ecb127e7ec01d73f35c1b921",
"pubkey": "88d7015a50f6bc0b5063e08d4423093c80862c83f18073fd287fccbbe87324ac",
"created_at": 1764123748,
"kind": 1,
"tags": [
[
"p",
"e5e66d799f4bebb72d7e00e44357c80ed698adc2acc69d98bf805da18d9445af",
"wss://relay.ditto.pub/"
],
[
"p",
"7d23b2dbb4b274388ff81c6db82fb0702cacb80de314d62e4be362189c6f6998",
"wss://relay.ditto.pub/"
],
[
"p",
"c002c4fe95bf086b31a84a5e7e68a0b4b4f58aee436323392038207880c2709a",
"wss://relay.ditto.pub/"
],
[
"e",
"308aef32a358c0ce8b8754a611ca2031c336ae0daaca3e39aa3ca6e0f1a5cf8e",
"wss://relay.ditto.pub/",
"reply"
],
[
"proxy",
"https://gamerplus.org/users/screwlisp/statuses/115613613952004907",
"activitypub"
],
[
"client",
"Mostr",
"31990:6be38f8c63df7dbf84db7ec4a6e6fbbd8d19dca3b980efad18585c46f04b26f9:mostr",
"wss://relay.ditto.pub/"
]
],
"content": "nostr:nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyrj7vmtena97hded0cqwgs6heq8ddx9dc2kvd8vch7q9mgvdj3z67jx00p2 Hopefully I was not too far off base, though I floundered at conveying what was going on with ACL2 functions needing to be total, and what that meant viz guards (and using acl2 primitives like zp for their guards).\n\nThanks for providing the dates, actual university and such live, I think I said 1980 when I meant 1990 which you corrected.\n\nI was pleasantly surprised by nostr:nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyp7j8vkmkje8gwy0lqwxmwp0kpczet9cph33f43wf03kyxyuda5esf9w3ml 's topics on the day I had been planning to miss but I was not prepared to opine on ACL2.",
"sig": "1c472f489a492c20ef69cc9f17b70449f1dbf1ef63c760ed8da780db7bea1e8cd719f3631c30fe982e9c70b6ab58ad15c33c3439a3b97f5bc6e70fc3449f44ac"
}