Recently there was no highlighting for operators with termination problems, and now there is no highlighting for operators with unsolved meta variables. Example:

 module Bug where

 foo_ : {a : Set} -> Set1 -> Set1
 foo_ x = x

 bar : Set1
 bar = foo Set

The last occurrence of foo should be highlighted, but it is not.

The reason for these problems is that operator ranges are represented in a stupid way. We can fix the particular problem above with another hack, but I would prefer if the root of these problems could be fixed.

Page last modified on June 01, 2007, at 12:59 AM
Powered by PmWiki