[Agda] Closures

[Vag Vagoff]

> Stop quantifying over Σ and Ω in the local functions:
>
>   execute {Σ} {Ω} input machine = …
>    where
>
>       loadTape : List Σ → Tape Σ
>       ⋮
>

Aha! I understood, thanks. Trick is expose Σ and Ω to local scope.