Default implicit types?

Stream: lean4

[François G. Dorais]

This is currently a wild idea. I'd like to hear public opinion before even trying to implement this. The idea is to have a notation for the default type of implicit variables.

The problem is summarized in this example extracted from Nat lemmas. This declaration

theorem lt_of_add_lt_add_left {k n m : Nat} : k + n < k + m → n < m := sorry

needs the implicit binders to infer the type (technically {k : Nat} would suffice but that's a bit weird). However, other declarations don't need this because of some random constant in the fold:

theorem lt_add_of_pos_right (h : 0 < k) : n < n + k := sorry

I would like to be able to write something like the following to specify the default type of all implicit variables.

theorem lt_of_add_lt_add_left {Nat} : k + n < k + m → n < m := sorry

There is no confusion with implicit variable declaration since Nat is already defined. Better yet, but perhaps wishful thinking, adding variable {Nat} at the start of a section or file to handle default types.

What do you think? I'm sure I haven't thought about all the possible side effects and issue, I'm also open to other notation since I already see confusion from overusing {_}.

[François G. Dorais]

Maybe {_ : Nat} would be clearer notation?

[Mario Carneiro]

you can write

theorem lt_of_add_lt_add_left : (k : Nat) + n < k + m → n < m := sorry

to get the type right while still getting the variable by autoImplicit, which seems sufficient to me