[Agda] missing double definition

[Andreas Abel]

You can do things like

f : ℕ
f = let m : ℕ
         m = 0

         m : ℕ
         m = 1 + m   -- reassign m
     in
     m

Whether this form of shadowing is good or bad, is up to dispute.

Cheers,
Andreas

On 10.01.2016 13:45, Sergei Meshveliani wrote:
> People,
> in the program of
>
> ------------------
> f : ℕ
> f = let m : ℕ
>          m = 0
>
>          m : ℕ
>          m = 1
>      in
>      m
> ------------------
>
> the value  m  is doubly defined.
> Need the type checker report an error?
>
> (Development Agda of January 9, 2016, ghc-7.10.2
> type-checks this).
>
> Thanks,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


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

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

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