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
17 stars 11 forks source link

Move Drinkers' Paradox to Predicate, change path to/from Inequalities, and adapt story line accordingly #3

Closed TentativeConvert closed 1 year ago

TentativeConvert commented 1 year ago

Commit 6077e5e introduces an additional level into Predicate: push_neg_abstract. I mainly wanted to introduce the notation P: X → Prop before it is used in the final level (Drinkers' Paradox) of Predicate. The level compiles, but I'm not sure I got the branching syntax correct.

abentkamp commented 1 year ago

Some files seem to be missing , e.g. the two push_neg levels and drinkers paradox.

TentativeConvert commented 1 year ago

Sorry. Files should now be present.

abentkamp commented 1 year ago

Thanks, the branching syntax looks correct.

abentkamp commented 1 year ago

@joneugster Can be merged, right?

joneugster commented 1 year ago

Yes, I think I was just waiting a few days to see if there were comments on my changes and then forgot to hit merge