Andrew Helwer on Nostr: npub1tkze6…ncd27 This is in the context of Lean! I have a pretty good idea of what ...
npub1tkze6tszqp7vlw48tv2537qttppxysym0jptfwak0z7r9wv79tss6ncd27 (npub1tkz…cd27) This is in the context of Lean! I have a pretty good idea of what polymorphic function means, it's just a function that takes a type as a parameter (like vec::<int>::append(x)) but "instance implicit argument" is giving me trouble. I think it has to do with the hints you can give to Lean's compiler about which concrete instance of a polymorphic function to use. In the case of the instance being implicit I guess you give no hints and let type inference figure it out.
Published at
2023-07-13 20:52:21Event JSON
{
"id": "97fd014cc4533714f3130b6949012faf5625ebe7b9a1af401e31c4be0ff7e1d8",
"pubkey": "6235fe36d733665c235dbec5983d768400cdb414ea18e0633cfe9d9c1ac6b02d",
"created_at": 1689281541,
"kind": 1,
"tags": [
[
"p",
"5d859d2e02007ccfbaa75b1548f80b584262409b7c82b4bbb678bc32b99e2ae1",
"wss://relay.mostr.pub"
],
[
"p",
"616c1b2daf1ac2d384a9a126a8e9d1e93ac700960bee8f28e855c06f59387e8e",
"wss://relay.mostr.pub"
],
[
"e",
"053c1e9e733f87e18dfb77e141232f942d9167989c309d5cd5d9736b7a95e7bc",
"wss://relay.mostr.pub",
"reply"
],
[
"mostr",
"https://fosstodon.org/users/ahelwer/statuses/110708755134550606"
]
],
"content": "nostr:npub1tkze6tszqp7vlw48tv2537qttppxysym0jptfwak0z7r9wv79tss6ncd27 This is in the context of Lean! I have a pretty good idea of what polymorphic function means, it's just a function that takes a type as a parameter (like vec::\u003cint\u003e::append(x)) but \"instance implicit argument\" is giving me trouble. I think it has to do with the hints you can give to Lean's compiler about which concrete instance of a polymorphic function to use. In the case of the instance being implicit I guess you give no hints and let type inference figure it out.",
"sig": "d036932277ff0dd9166a03cfed31a29c1d121422d960427c51daacdebf2992a34f8384de6ede574e3920aed117c8bd1de348d9c6e876ede10882bd31b40aa29c"
}
