search

hhu-adam / Robo

A game for learning lean 4 where a cute little Robo joins you on your exploration of the Mathiverse. The game is in German 🇩🇪
https://adam.math.hhu.de
Apache License 2.0
16 stars 9 forks source link

Cantor, level 9: Cantor says „Gute Wahl“ also for incorrect choices #51

Open TentativeConvert opened 2 months ago

TentativeConvert commented 2 months ago

For example, writing

let c : A → Y := fun a ↦ f a a

as first line also leads to this positive but misleading reaction of Cantor.