[Agda] Re: Agda with GHC-6.10.4, continued...

kahl at cas.mcmaster.ca kahl at cas.mcmaster.ca
Mon Apr 12 17:44:39 CEST 2010


On Mon, 12 Apr 2010, Nils Anders Danielsson <nad at Cs.Nott.AC.UK> wrote:
 > On 2010-04-09 21:58, kahl at cas.mcmaster.ca wrote:
 > > I succeeded to get Agda installed with GHC-6.10.4 after that, but now
 > > pattern matching on pairs does not work anymore [...] The missing
 > > patches are: [...]
 > 
 > I believe those patches are unrelated to pattern matching for record
 > types, which was introduced by the patch named "allow pattern matching
 > on records (doesn't obey eta equality yet)".

However, these patches did make the difference.
Even though the introducing patch will still have been there
(and I used pattern matching on pairs successfully before),
something in the listed patches probably kept pattern matching on records
enabled for some other recent change...

At least for me, this is now not important anymore
since I now have GHC-6.12 (currently 6.12.1.20100330) also on PowerPC.

Thanks for looking into this!


Wolfram


More information about the Agda mailing list