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 10 forks source link

Term Modus and forward reasoning #1

Open joneugster opened 1 year ago

joneugster commented 1 year ago

We need to explain basic term modus at some point.

In particular people find it hard to distinguish between backwards argumentation (apply) and forward argumentation (not nicely implemented yet).

Maybe the syntax have j := even_squared h or replace h := even_squared h would be good to introduce?

TentativeConvert commented 10 months ago

For forward reasoning, we should in any case introduce 'apply at', now that it's in mathlib.