Parameterised Blocks/Modules?

Stream: lean4

[Ellis Kesterton]

Is there any feature in Lean4 that would allow me to parameterise a bunch of definitions by the same type, in the style of Agda modules or Idris parameter blocks? The "variable" construct does not quite do what I want, since within the scope of the variable I must keep instantiating my types with the variables.