id : {A : Set} -> A -> A
id = { λ { {A} x → x} }0
-- refining the above gives
-- λ {A x → x}
-- instead of
-- λ { {A} x → x}
I've attached a patch that fixes this, keeping the Hiding information that was lost in the translation to Concrete syntax and ensuring we get a space between "λ {" and "{A}".
From sanzhi...@gmail.com on September 08, 2013 06:39:34
id : {A : Set} -> A -> A id = { λ { {A} x → x} }0 -- refining the above gives
-- λ {A x → x}
-- instead of
-- λ { {A} x → x}
I've attached a patch that fixes this, keeping the Hiding information that was lost in the translation to Concrete syntax and ensuring we get a space between "λ {" and "{A}".
Attachment: fix-printing-of-extended-lambdas-starting-with-an-hidden-argument.dpatch
Original issue: http://code.google.com/p/agda/issues/detail?id=898