[Agda] Associativity for free!

[Alan Jeffrey]

On 10/26/2011 04:01 PM, James Chapman wrote:
> 1. A trivial solution for your example is simply to make _++_ associate to the left:

Indeed. Unfortunately, sometimes it's convenient one way round, and 
sometimes the other. No matter which way you pick, it'll go wrong half 
the time :-)

> 2. Another solution I learnt from Conor (exercise 15, his AFP notes http://www.strictlypositive.org/epigram-notes.ps.gz) is simply to avoid it.

Hmm, I can see that this might work, though some lemmas (e.g. 
substitution commuting with weakening) would need a bit of work. Of 
course at this point having hacked out a version of lists with 
associativity, I'd like to keep pushing on it to see if I can get the 
properties I need to go through.

 > Alan: neat trick!

Thanks!

A.