[Agda] `where' scope

[Andreas Abel]

Sounds like a bug in MAlonzo, can you report it on the bug tracker?
Thx, Andreas

On 24.09.12 10:13 PM, Serge D. Mechveliani wrote:
> People,	
> 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-2.3.0.1 MAlonzo  reports a  multiple definition of  f.

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/