[Agda] Weird behaviour inside of ‘let’

Mateusz Kowalczyk fuuzetsu at fuuzetsu.co.uk
Sun Jan 19 09:46:32 CET 2014


Hi,

I was turning some expressions of the form ‘foo = λ a b c → f c b a’
that I had inside a let into the ‘foo a b c = …’ form but I
encountered a rather weird behaviour, ranging from things being
claimed not in scope to parse errors. See [1] for some snippets. Can
someone explain these?

[1]: http://lpaste.net/98754

--
Mateusz K.


More information about the Agda mailing list