|
|
|
|
|
|
by taejo
117 days ago
|
|
|
The point GP is making, is that everyday mathematics is not done in Lean, but in a language that's more like JavaScript, where equals doesn't always mean equals, + and • mean whatever seems convenient at the time, and objects sometimes change type without notice. |
|
|