Hiding section variables

Stream: lean4

[Craig McLaughlin]

I'm struggling to develop a nice way of hiding section variables in a development where I require them to be explicit and implicit at various times. The issue is best illustrated with a small example:

universe u
variable (σ α ρ ξ ω : Type u)
         [Inhabited σ] [Inhabited α] [DecidableEq α]
         [Inhabited ρ] [DecidableEq ρ]
         [Inhabited ξ] [DecidableEq ξ]
         [Inhabited ω]

structure IOAutomaton where
  init : σ
  step : σ → α → ρ × σ

structure Machine extends IOAutomaton σ α ρ where
  active : σ → List ξ
  dom : α → ξ
  obs : ξ → σ → ω

-- How to hide the variables but keep the constraints?
abbrev IO' (M: Machine σ α ρ ξ ω) := Machine.toIOAutomaton M
#check IO'
-- IO' : (σ α ρ ξ ω : Type u) (M : Machine σ α ρ ξ ω) : IOAutomaton σ α ρ

I want to use a Machine in subsequent definitions so I create a small abbreviation for conciseness. However, it forces me to specify the variables rather than infer them implicitly. Can I avoid this behaviour? I want the definitions of IOAutomaton and Machine to be explicit in the type variables, and I have definitions further down that need the explicit variables as well.

In other parts of my development, I have used sections in the middle of the file to introduce the same collection of variables and constraints but making the variables implicit. I'd rather not do this every time, and I'm hoping there's already a better way I just don't know about.

[Sebastian Widua]

you can turn them into implicit variables by doing this

abbrev IO' {σ α ρ ξ ω} (M: Machine σ α ρ ξ ω) := Machine.toIOAutomaton M

[Sebastian Widua]

note that the Inhabited and DecidableEq constraints only get included if you actually need them inside the definition