[Agda] `where' scope

Serge D. Mechveliani mechvel at botik.ru
Mon Sep 24 22:13:30 CEST 2012

how does this occur that `where' does not protect its local scope?
Thus, for
  f : Nat -> Nat
  f = suc
  g : Nat -> Nat
  g x =  f $ suc x  where
                    f : Nat -> Nat
                    f y = y

Agda- MAlonzo  reports a  multiple definition of  f.
It is natural to put that a value defined under `where' is local and
overrides the outer value of the synonym (like in Haskell).

What is a profound reason to change this nice rule?

May be `private' will help, but why does one need to put an extra 
`private' ?



More information about the Agda mailing list