Ability to Normalize an expression within the current scope

[laserbat]

Currently, Normalize (C-c C-n) operates in the global scope by default. If I have

module Booleans where
  data Bool : Set where
    false : Bool
    true : Bool

  not : Bool → Bool
  not false = true 
  not true  = false 

I can't simply normalize an expression like not (not false); instead, I have to use Booleans.not (Booleans.not Booleans.false), which is cumbersome.

The scope is selected correctly when C-c C-n is called from a hole. This is a decent workaround, but it would be much more convenient if there were an alternative Normalize command that automatically took the current scope (as determined by the cursor position) into account.

I'm not very familiar with Agda, so excuse me if this is a nonsensical request or if there's a technical limitation preventing this feature from being implemented.