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
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