parameter vs variable

Stream: lean4

[Cyril Cohen]

In Lean3 there used to be both parameter and variable, Lean4 has only variable, I was wondering what motivated that change and whether mathlib developers were happy with that?

[Patrick Massot]

I think the story is: parameter didn't really work in Lean 3 so we didn't use them. Then Lean 4 developers decided that fixing parameter was not worth the trouble since we were happy without using it, hence they removed it.

[Cyril Cohen]

Thanks @Patrick Massot