google-code-export / omega

Automatically exported from code.google.com/p/omega
Other
2 stars 0 forks source link

record printing flawed in error message #42

Closed GoogleCodeExporter closed 9 years ago

GoogleCodeExporter commented 9 years ago
Sometimes I get this error message:

While type checking in the scope of:
   stopHead PlusL { PlusL:PlusR PlusR:PlusR PlusL:PlusR }lm Eq
We need to prove:
   Equal {}r {0t=2t}r, Equal 0t 0t, Equal 0t 0t

The second line should read:

   stopHead PlusL {PlusL=PlusR, PlusR=PlusR, PlusL=PlusR}lm Eq

Just for the record :-)

Do not bother fixing this, I shall put together a patch soon.

Original issue reported on code.google.com by ggr...@gmail.com on 6 Dec 2007 at 2:07

GoogleCodeExporter commented 9 years ago
Here you go. This patch works and is pretty.

Original comment by ggr...@gmail.com on 6 Dec 2007 at 4:40

Attachments:

GoogleCodeExporter commented 9 years ago

Original comment by ggr...@gmail.com on 9 Dec 2007 at 8:50

GoogleCodeExporter commented 9 years ago
fixed on trunk with r143

Original comment by ggr...@gmail.com on 16 Jul 2008 at 9:04

GoogleCodeExporter commented 9 years ago
Never seen this in 1.4.6.

Original comment by ggr...@gmail.com on 3 Feb 2011 at 10:26