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

FunctionSurj, Level 1: Type of f is not displayed. #54

Open TentativeConvert opened 1 month ago

TentativeConvert commented 1 month ago

It is impossible to see from the proof state what domain and codomain of f are intended:

image

The hints make clear that it is supposed to be a function ℤ → ℤ. Is there a way to make this visible in the goal? Otherwise, how is the user supposed to infer this without switching to editor mode and looking at the actual statement in lean? (I guess lean does infer these types from x : ℤ and f x being comparable to x?)

joneugster commented 1 month ago

There are hover pop-ups that should show the type, I think. But rn on dev these popups are hidden behind the goal and therefore invisible.

I believe there is a (pp-) option in Lean to turn this on globally for the game, but it might be quite verbose.

TentativeConvert commented 1 month ago

The hover pop-up is visible on the live server: image But this is still miles away from what is written in the chat: image I think we either need to revert to our old habit of displaying the statement image at the top of the exercise, or add an additional zeroeth level that introduces the notation f: A → B for functions. (My preference would be the additional level.)

joneugster commented 1 month ago

I think the option I was thinking of is something line set_option pp.binderType true or something. That might be worth trying out too. (regardless of an additional öevel being added)