Taneb on Nostr: I'm trying to implement an Agda-like language in Agda, starting by defining a type of ...
I'm trying to implement an Agda-like language in Agda, starting by defining a type of well-typed expressions. I feel like every turn I realise new subtleties. It's a learning experience.
Published at
2024-09-22 07:34:16Event JSON
{
"id": "fcdb73d39b4391a3d3e0dcbfc29b99ce7369f74144e21c0ccf6e51d708821121",
"pubkey": "89a426aa0bd043f97191032ea71032f170a27a25fe68924646a34dc50b8056cf",
"created_at": 1726990456,
"kind": 1,
"tags": [
[
"proxy",
"https://hacksrus.xyz/objects/2833fe81-d199-4bf2-add3-3385d4a40ed0",
"activitypub"
],
[
"L",
"pink.momostr"
],
[
"l",
"pink.momostr.activitypub:https://hacksrus.xyz/objects/2833fe81-d199-4bf2-add3-3385d4a40ed0",
"pink.momostr"
],
[
"-"
]
],
"content": "I'm trying to implement an Agda-like language in Agda, starting by defining a type of well-typed expressions. I feel like every turn I realise new subtleties. It's a learning experience.",
"sig": "ba400ab7841748cb9715f8fee504f2b4397d3afea58b27af148634111c5333fb6834ae4cf49266f2cb6f7d1617690ac7c2bbc0e246bf9a8a9eef3ebe0d151991"
}
