search

UlfNorell / agda-test

Agda test
0 stars 0 forks source link

pretty printing module applications bug #902

Closed UlfNorell closed 10 years ago

UlfNorell commented 10 years ago

From sanzhi...@gmail.com on September 16, 2013 21:38:45

module Bug where

module M (A : Set) where

postulate A : Set F : Set -> Set

test : A test = {! let module m = M (F A) in ? !} -- C-c C-r gives let module m = M F A in ? -- instead of let module m = M (F A) in ?

The attached patch fixes this by passing the right Precedence for the components of the module expression.

It might be better to produce the application as an Abstract.Expr and call toConcrete on that instead, if there's a good way to turn ModuleName into Abstract.QName.

Attachment: fix-printing-of-module-applications.dpatch

Original issue: http://code.google.com/p/agda/issues/detail?id=902

UlfNorell commented 10 years ago

From nils.anders.danielsson on September 17, 2013 02:56:09

Applied.

Status: Fixed

UlfNorell commented 10 years ago

From nils.anders.danielsson on September 19, 2013 06:37:38

Labels: Display

UlfNorell commented 10 years ago

From andres.s...@gmail.com on November 11, 2013 06:25:10

Labels: Type-Defect