variable {C}

Stream: lean4

[Kevin Buzzard]

Here's a change from Lean 3:

variable (C : Type) [Inhabited C]

example : C := arbitrary

variable {C}

example : C := arbitrary -- fails
/-
failed to synthesize instance
  Inhabited C
-/

If I change the default binder for C then I lose the type class [Inhabited C]. Is this expected behaviour?

[Back story: I'm manually porting some category theory to Lean 4 and initially I thought we were back in the 2019 hell of having to include 𝒞 when universes got hairy, made even worse here by the fact that include might not have made it to Lean 4 yet (?). I then realised that in fact
something far simpler was going on :D . In fact Lean 4 universes seem to be working fine in category theory so far.]

[Marc Huisinga]

You didn't really change the default binder, you declared a new C, right?
E.g. in the first example C : Type and in the second one C : Sort u.

[Daniel Selsam]

FYI this was added to Lean3 @ https://github.com/leanprover-community/lean/commit/dc93603b4af3f0ed4559d48fe3d55e4e68ffbdfb

[Kevin Buzzard]

@Marc Huisinga this is my point -- in Lean 3 this works fine

variables (C : Type) [inhabited C]

example : C := arbitrary C

variable {C}

example : C := arbitrary C

and this idiom is used quite a bit in mathlib -- you develop some theory about groups with (G : Type*) [group G] and then you want to develop some stuff involving (g : G) so you write variable {G} and now G is still a group but it's implicit in the lemmas where it's included from that point on. So I thought I did change the default binder. I don't understand Daniel's link -- C or C++ or whatever it is is all greek to me.

[Daniel Selsam]

Kevin Buzzard said:

I don't understand Daniel's link -- C or C++ or whatever it is is all greek to me. Update: aah! I understand the tests though :-)

Sorry for the curt response above :) -- In addition to the tests, the commit message links to the original GitHub issue that motivated the feature (https://github.com/leanprover/lean/issues/532).

[Daniel Selsam]

I recommend creating a Lean4 issue for the feature.

[Kevin Buzzard]

lean4#536

[Daniel Selsam]

Does anyone else find that this topic keeps getting removed from the #lean4 stream list? It looks like a bug in Zulip, probably triggered by the braces in the topic name.

[Daniel Selsam]

Kevin Buzzard said:

lean4#536

Note: the syntax highlighting isn't working in your issue for some reason.

[Marc Huisinga]

Kevin Buzzard said:

Marc Huisinga this is my point -- in Lean 3 this works fine

Ah, sorry :) I wasn't sure if you had already noticed that it's unrelated to the type class.

[Kevin Buzzard]

Another weird thing: I _did_ click on the "#532" link on github (the one which Daniel pointed out in his second post), but when I did it, it took me to https://github.com/leanprover-community/lean/pull/532 (the fork) which is unrelated, and this was what caused my "I don't understand anything" outburst.

[Kevin Buzzard]

Daniel Selsam said:

Kevin Buzzard said:

lean4#536

Note: the syntax highlighting isn't working in your issue for some reason.

On Zulip ``` is enough, but on github I need ```lean . I fixed it.

[Daniel Selsam]

Kevin Buzzard said:

Another weird thing: I _did_ click on the "#532" link on github (the one which Daniel pointed out in his second post), but when I did it, it took me to https://github.com/leanprover-community/lean/pull/532 (the fork) which is unrelated, and this was what caused my "I don't understand anything" outburst.

That was my fault -- I should have originally linked to the commit from the leanprover repo instead of the leanprover-community repo so that the issue link would work.