A game for learning lean 4 where a cute little Robo joins you on your exploration of the Mathiverse. The game is in German 🇩🇪
16
stars
9
forks
source link
Quantus, Level 6: explain why 'use n^2/2' does not work #19
Closed
TentativeConvert closed 4 months ago
Add a branch to catch this command, and explain in a hint that division is not defined on natural numbers.