Tariq on Nostr: Back to learning #Lean4 I gave up on the "positivity/extra" thing because sadly like ...
Back to learning #Lean4
I gave up on the "positivity/extra" thing because sadly like many languages "making easy things easy" isn't a current priority for the devs.*
I'm now learning about structured proofs, starting with creating intermediate results.
( * one of the courses creates fake commands to remedy this, and I recall I created a simple.js layer for p5js for this same reason )
#maths
Published at
2024-08-12 18:08:35Event JSON
{
"id": "639603273914b06131018ab8f4833cbdf49286535ecdbbf81ddd70f8c7a539df",
"pubkey": "340694a5c7115fe0918fe7ec9038786592e3804f1a0e457e3e09d03ecfdadc6b",
"created_at": 1723486115,
"kind": 1,
"tags": [
[
"t",
"lean4"
],
[
"t",
"maths"
],
[
"proxy",
"https://mastodon.social/users/rzeta0/statuses/112950386052849781",
"activitypub"
]
],
"content": "Back to learning #Lean4 \n\nI gave up on the \"positivity/extra\" thing because sadly like many languages \"making easy things easy\" isn't a current priority for the devs.*\n\nI'm now learning about structured proofs, starting with creating intermediate results.\n\n( * one of the courses creates fake commands to remedy this, and I recall I created a simple.js layer for p5js for this same reason )\n\n#maths\n\nhttps://files.mastodon.social/media_attachments/files/112/950/374/608/571/840/original/e33b21ea57beb58c.jpg",
"sig": "fc980cd4f596a270bff071f4c7247681fd87fd3f7195f5ff94f81f3a8761716ab652d8dcb301f536cd15f37506c9cb6d08078ccfb0cd339467b2f39df36e5ff1"
}
