yes
data MyList : Nat -> Type -> Type where
Nil : MyList n x
(::) : x -> MyList n x -> MyList (S n) x
azul
npub1e9…2vdd5
2025-02-03 16:21:51 UTC
in reply to nevent1q…rz2l
Author Public Key
npub1e9y64jhalql35k2cfhntmkvnnz5937pwrq0267578qrpty6uafzsc2vdd5Seen on
wss://relay.momostr.pinkPublished at
2025-02-03 16:21:51 UTCEvent JSON
{
"id": "148f02e668694bd1a3610c202d27d4b5ff6dad2cc789f4efdf5aca5ce6f686ec",
"pubkey": "c949aacafdf83f1a59584de6bdd99398a858f82e181ead7a9e380615935cea45",
"created_at": 1738599711,
"kind": 1,
"tags": [
[
"proxy",
"https://gamedev.lgbt/@typeswitch/113940870706062880",
"web"
],
[
"p",
"6bdab9eda962efa7ecc9ae53ce8c59b532593a8473b564f76aa9d0b44862a35c"
],
[
"e",
"a9ebd4ce581a5e75c179bb4efc9200f5b6a2e1f0bcf992526077ea6ecca8e13e",
"",
"root",
"6bdab9eda962efa7ecc9ae53ce8c59b532593a8473b564f76aa9d0b44862a35c"
],
[
"proxy",
"https://gamedev.lgbt/users/typeswitch/statuses/113940870706062880",
"activitypub"
],
[
"L",
"pink.momostr"
],
[
"l",
"pink.momostr.activitypub:https://gamedev.lgbt/users/typeswitch/statuses/113940870706062880",
"pink.momostr"
],
[
"-"
]
],
"content": "yes\n\ndata MyList : Nat -\u003e Type -\u003e Type where\n Nil : MyList n x \n (::) : x -\u003e MyList n x -\u003e MyList (S n) x",
"sig": "5af80e9a3284d0ab576addf03c27cf933c25fa5fcedda53bb895b12db656235348ab22cf48ca977df0ee43bc8ff72a20ca76c907e3a28b550b9d9f59fa47aa33"
}