Jesper Agdakx 🔸 on Nostr: #Agda hivemind please help me: what is the correct definition of the Delay monad ...
#Agda hivemind please help me: what is the correct definition of the Delay monad transformer? Is it
DelayT : (m : Set → Set) (a : Set) (i : Size) → Set
DelayT m a i = Delay (m a) i
or
DelayT : (m : Set → Set) (a : Set) (i : Size) → Set
DelayT m a i = m (Delay a i)
?
Published at
2024-01-18 16:33:22Event JSON
{
"id": "36fcbd4fd36cee11c7e4c4428380bc1ff952a921d091b14d57097057ba24737e",
"pubkey": "2a1e7bc1546b32c5b09fdd4ac64745041dfece34e5f82d70027fa05539b008b9",
"created_at": 1705595602,
"kind": 1,
"tags": [
[
"t",
"agda"
],
[
"proxy",
"https://agda.club/objects/23d3b764-3f75-4bb0-8fba-8836d95d661c",
"activitypub"
]
],
"content": "#Agda hivemind please help me: what is the correct definition of the Delay monad transformer? Is it\n\nDelayT : (m : Set → Set) (a : Set) (i : Size) → Set\nDelayT m a i = Delay (m a) i\n\nor\n\nDelayT : (m : Set → Set) (a : Set) (i : Size) → Set\nDelayT m a i = m (Delay a i)\n\n?",
"sig": "42293a4d74403ca98f95185ce90b317d63b50faa73ba7d256cce8b9e68fe3e1c8964f0a62b22fbcaacb023870210f1ee800b06bad1171cc9f7d71478b6ad74d3"
}
