Explicit/implicit argument of Inhabited.default

Stream: mathlib4

[Gabriel Ebner]

In Lean 3, inhabited.default had an explicit argument for the type. In Lean 4, this argument is implicit now. Unless I'm missing something, this means we need to backport the change to Lean 3 core, right?

[Gabriel Ebner]

Alternatively, we could also 1) align the Lean 3 definition with a new default' definition in mathlib4, or 2) hack this in as a special case in synport.

[Mario Carneiro]

I think there is value in both versions. There is also arbitrary, which isn't used much in lean 3

[Mario Carneiro]

We should try to get consistency, but I'm not sure whether to port forward or backward, and whether we need a default'

[Gabriel Ebner]

I'm somewhat concerned that we might be running into problems with arbitrary at some point (since it is a constant and you can't prove anything about it).

[Mario Carneiro]

Also I think default is exported in lean 3 but not lean 4

[Mario Carneiro]

I guess it's not terrible to have only the implicit version, since (default : A) isn't that much harder to write than default A

[Gabriel Ebner]

We should try to get consistency, but I'm not sure whether to port forward or backward, and whether we need a default'

I think default' is the worst option here, we don't need yet another name for the inhabited value (we already have arbitrary and default).

Porting forward backward isn't too hard, there's only 668 occurrences of the word default in mathlib.

[Mario Carneiro]

porting forward would mean replacing uses of default in lean 4 core and mathlib4

[Gabriel Ebner]

There's a lot of default _ in mathlib, so I'd tend to the implicit version. (We even have (default _ : C).....)

[Mario Carneiro]

I agree, it looks like at least 1/3 of uses are default _ and maybe another 1/3 or more supply it although it is not necessary

[Gabriel Ebner]

https://github.com/leanprover-community/lean/pull/660