[Agda] local needs override

Serge D. Mechveliani mechvel at botik.ru
Tue Sep 25 19:51:13 CEST 2012

it is more natural for a local binding to prevail (as in Haskell).
Here I provide an argument beyond that "because Haskell is so".

Imagine that nowdays a child says: "where is mother?".
Which mother he more probably means, his "local", or may be mother of 
king James ?
An English girl says "yesterday it swimmed".
What she more probably means: a rain in her town, or may be a rain in 
South America?

On average, it is _more often_ occurs that a local thing is meant rather 
than a global.
This is why it is better for a local binding to prevail.
Similar is in programming.



More information about the Agda mailing list