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

[TentativeConvert]

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

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]

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]

The hover pop-up is visible on the live server:

But this is still miles away from what is written in the chat:

I think we either need to revert to our old habit of displaying the statement

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]

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)