[Agda] Panic: CanSplit

[Wouter Swierstra]

>
>  Panic: CantSplit Tmp.Step
>
> Is this with a recent version of Agda? I thought I had fixed these  
> error messages to make more sense.

Updating Agda resulted in a much better error message - thanks Ulf!

I managed to solve my original problem this morning by defining the  
following alternative version of less-than-or-equal-to:

> data _<=_ : {n : Nat} -> Fin n -> Fin n -> Set where
>  Base : forall {n : Nat} {i : Fin n} -> fz <= i
>  Step : forall {n : Nat} (i j : Fin n) -> i <= j -> fs i <= fs j

and showing that the two definitions are equivalent. I can't help but  
wonder if there is some clever trick I'm missing.

   Wouter