Hi Thorsten
Thorsten Altenkirch wrote:
I jsut discovered a new bug, which seems to be related to the recent changes.
I tried using the new facility, of being able to interactively use implicit parameters.
However, the assignment between visible names and Horace 's names seems to
be getting out of sync, i.e.
The following illustrates a number of dangers, the first of which is the typographical mess caused by sending wide Epigram source in emails.
( bs : List A !
let !-----------------------------------------------------------------------!
! assocAppend _bs : append as (append bs cs) = append (append as bs) cs )
assocAppend _ bs <= rec bs' { assocAppend _ bs [] } Strangely, Horace reports that bs:* , surely he means A...
Any road up, there is a bug, but it's not what you seem to think it is. By writing the declaration as you do, you're suggesting that bs should be the first implicit argument of assocAppend. This is impossible, so the bug is that your declaration was not rejected. Clearly, A must come before bs. Actually, Epigram seems to figure out something of the sort, which is presumably why bs is taken to be the name of the type argument.
By the way, what makes you think any of the arguments to appendAssoc other than A stands any chance of being inferred? There's no way Epigram will unify as, bs and cs when they sit underneath the function append.
I've just checked that the sensible way to state and prove this theorem works without difficulty. I haven't attached the file, as I suspect this may be an exercise in the making...
Cheers
Conor
PS Just back from the Agda implementors' meeting. It was lots of fun and very productive. We should have one.
-- http://www.cs.rhul.ac.uk/~conor
