search

leanprover-community / lean4game

Server to host lean games.
https://adam.math.hhu.de
GNU General Public License v3.0
177 stars 32 forks source link

Multivariables in Infoview #105

Open joneugster opened 1 year ago

joneugster commented 1 year ago

Add an option to never show A B : Type in the infoview but rather two lines A : Type and B : Type. Disable the option by default but enable it in the NNG.

kbuzzard commented 1 year ago

I've seen no example in NNG4 where there are more than 3 terms of a given type BTW.

joneugster commented 12 months ago

I can't quite get myself to like this idea yet, I personally prefer A B C : Type much more.

@TentativeConvert @abentkamp any thoughts?

TentativeConvert commented 12 months ago

I don't see any advantage of writing A : Type and B : Type, expect that A B : Type might require one additional line of explanation, once. Is that the motivation? I would certainly want A B : Type to remain the default.

abentkamp commented 12 months ago

The notation is indeed a bit confusing because space normally means application, and here it is just a list. But I haven't ever heard newcomers complain about it. @kbuzzard would know better if this is really something that can confuse people.