Of the New Day is a song of rebirth, emerging from darkness. It sounds deceptively simple, a recognisably atypical Porcupine Tree ballad. That is until you realise that the length of the bars is constantly changing, flipping between bars of regular 4/4 time to 3/4, to 5/4 to 6/4, 11/4, so that the track never settles into any steady time. It’s what PT can sometimes do really well, come up with a basic idea that’s almost intellectual or mathematical, but carry it off in a way that sounds completely natural and accessible.
Schlagwort: Mathematik
Aus den Takten.
Leanorris.
Hey! I heard that Lean thinks 1/0 = 0. Is that true?
Yes. So do Coq and Agda and many other theorem provers.
[...]
But doesn’t that lead to confusion?
It certainly seems to lead to confusion on Twitter. But it doesn’t lead to confusion when doing mathematics in a theorem prover. Mathematicians don’t divide by 0 and hence in practice they never notice the difference between real.div and mathematical division (for which 1/0 is undefined). Indeed, if a mathematician is asking what Lean thinks 1/0 is, one might ask the mathematician why they are even asking, because as we all know, dividing by 0 is not allowed in mathematics, and hence this cannot be relevant to their work.
Nice but late.
“But there is no honor in elegantly proving a theorem in 1672 that some Scotsman proved barbarously in 1671!”
Neal Stephenson: Quicksilver
No arrows, not even objects.
Am I the only one who annoyed by "functor" in Prolog?
Teilen mit Rest.
Bistromathics itself is simply a revolutionary new way of understanding the behaviour of numbers.
Douglas Adams: The Restaurant at the End of the Universe