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

Implis 13: add `imp_iff_not_or` to Inventory #28

Closed TentativeConvert closed 3 months ago

TentativeConvert commented 3 months ago

The level conists of a proof of https://leanprover-community.github.io/mathlib4_docs/Init/PropLemmas.html#Decidable.imp_iff_not_or. This would be a natural lemma to use in the proof of the Drinker's paradox in the final level of Predicate/Quantus.

joneugster commented 3 months ago

It's in the inventory, just under the [anonymous] tab because it's in no namespace and no documentation has been written.

joneugster commented 3 months ago

now I moved it to the "Logic" tab.