Unfold where

Stream: lean4

[Marcus Rossel]

I can't figure out how to unfold the definition of a function defined in a where clause in a proof:

example (n : Nat) : True := by
  have : double n = 2 * n := by
    simp [double]
  sorry
where
  double (x : Nat) : Nat := 2 * x

On simp [double] I get the error:

invalid 'simp', proposition expected
  ℕ → ℕ

How can I unfold double?

[Henrik Böving]

For a double that is defined outside of a where clause this proof works out by rfl but not for the one inside the where clause so I'm guessing that this use case isn't something that is supported at the moment?