[Agda] Pattern-matching, unfortunate effect on type

[Nils Anders Danielsson]

On 2010-01-28 17:53, Florent Balestrieri wrote:
> So after case-splitting agda does not give the same goal type
> for the same argument, as if some dependency was lost in the
> process.

I discussed this with Florent IRL. The problem was that a later pattern
had already refined the type of the pattern he was refining, and Agda is
sensitive to the order of pattern matching.

-- 
/NAD