[Agda] Panic: CanSplit

[Andreas Abel]

Hi Wouter,

maybe that is not what you want, but you can try heterogeneous  
inequality.

data _<=_ : {n m : Nat} -> Fin n -> Fin m -> Set where
  Base : {n : Nat}{i : Fin n} -> i <= i
  Step : {n m : Nat}{i : Fin n}{j : Fin m} -> i <= j -> fs i <= fs j

fsLt : forall {n : Nat} (i j : Fin n) -> fs i <= fs j -> i <= j
fsLt i .i Base = Base
fsLt i j (Step  d) = d

Cheers,
Andreas

On Jul 17, 2009, at 12:24 PM, Wouter Swierstra wrote:
> 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.


-------------- next part --------------
A non-text attachment was scrubbed...
Name: LeqFin.agda
Type: application/octet-stream
Size: 533 bytes
Desc: not available
Url : https://lists.chalmers.se/mailman/private/agda/attachments/20090717/ecc7e407/LeqFin.obj