[Agda] Panic: CanSplit

[Andreas Abel]

Sorry, the definition of <= was messed up in my last message, the  
correct definition of heterogeneous inequality is of course:

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 -> i <= fs j

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

On Jul 17, 2009, at 4:05 PM, Nils Anders Danielsson wrote:

> On 2009-07-17 14:31, Andreas Abel wrote:
>> 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
>
> This is equality, right?

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