U tweetove putem weba ili aplikacija drugih proizvođača možete dodati podatke o lokaciji, kao što su grad ili točna lokacija. Povijest lokacija tweetova uvijek možete izbrisati. Saznajte više
Among other things, this means that the very roles of abstraction, composition and encapsulation are drastically different from those they play in programming.
This also sets TLA⁺ apart from similarly-rich logics with proof assistants and/or model checkers that *are* based on programming, like Lean or Agda, and SPIN's Promella or NuSMV's language.
Yes, Lean is for serious formal "high" mathematics. I think it took me the same amount of time to learn TLA⁺ from scratch and write my first non-trivial spec as it took me to understand how quantifiers work in Lean, though.
You can implement TLA+’s logic in Lean.
Lean is more like math that you happen to be able to write programs in. To put it simply. 
I get what you’re saying though. It’s similarity hard for programmers to grasp Lean and the separation between program and specification.
Twitter je možda preopterećen ili ima kratkotrajnih poteškoća u radu. Pokušajte ponovno ili potražite dodatne informacije u odjeljku Status Twittera.
