Hi, Am Dienstag, den 26.02.2013, 10:25 +0100 schrieb Andreas Abel:
To your amusement, I found the following in the Agda source:
abstractToConcreteCtx :: ToConcrete a c => Precedence -> a -> TCM c abstractToConcreteCtx ctx x = do scope <- getScope let scope' = scope { scopePrecedence = ctx } return $ abstractToConcrete (makeEnv scope') x where scope = (currentScope defaultEnv) { scopePrecedence = ctx }
I am surprised this is a legal form of shadowing. To understand which definition of 'scope' shadows the other, I have to consult the formal definition of Haskell.
in more imperative looking Haskell code, I find it useful to shadow a previous binding by a new "foo <-" binding... People who do not like that should use -Wall (or a more specific flag like -fwarn-name-shadowing). Greetings, Joachim -- Joachim "nomeata" Breitner Debian Developer nomeata@debian.org | ICQ# 74513189 | GPG-Keyid: 4743206C JID: nomeata@joachim-breitner.de | http://people.debian.org/~nomeata