Innocuous question about weak implicits

Stream: lean4

[François G. Dorais]

This is a bit of a weird question. I was looking at some old code of mine and I somehow wrote something like this (irrelevant details omitted):

def widget {{t : α}} {x₁ x₂ : β} {{y : γ}} : bobloblawslawblog t x₁ x₂ y := sorry

This was a while ago so I don't remember what I was thinking. Perhaps I was just blindly applying internal rules about weak implicits, perhaps this is the result of some blind search/replace, or perhaps I really meant this alternation of strong and weak implicits. Regardless, I'm now rather puzzled what this mix of strong and weak implicit parameter means.

I'm thinking there is no real context where this is different from {{t : α}} {x₁ x₂ : β} {y : γ}. I'm not sure. I would really like to know how weak and strong implicit parameters work when interlaced.

PS: Sorry if that's in the docs somewhere. I didn't find it, but I might have been using the wrong keywords.

[François G. Dorais]

PPS: Actually it was a theorem not a def. I don't think that's very relevant.