[Agda] multiple definitions in `let'

[mechvel at scico.botik.ru]

Dear Agda team,

Is the below  f  a correct program?
(Agda 2.6.1  type-checks it).

module Test where
open import Data.Nat using (ℕ)

f : ℕ
f = let
       a = 1
       a = 2
     in
     a

  {-
f' : ℕ
f' = a
      where
      a = 1
      a = 2
  -}