[Agda] how do I handle absurd with patterns?

[Carter Schonwald]

Hey all,

i've a small development (a baby system f),
and I find myself with a case that looks like the following (full file
attached, key bit inline here)


τSubstFancy : ∀  { tfv } -> (barrier : Nat) -> TypeF (1  + barrier  + tfv )
-> TypeF ( barrier + tfv) -> TypeF (barrier + tfv )
τSubstFancy bar (vτ x) t  with compare bar (finToNat x)
τSubstFancy zero (vτ zero) t | less lt = {!!} -- this is the case i'm
stumped by
τSubstFancy zero (vτ (suc x)) t | less lt = {!!}
τSubstFancy (suc bar) (vτ x) t | less lt = {!!}
τSubstFancy bar (vτ x) t | equal eq = t
τSubstFancy bar (vτ x) t | greater gt = {!!}
τSubstFancy bar (∀τ tar) t = {!!}
τSubstFancy bar (tar →τ tar₁) t = {!!}

how do i deal with this  0 < 0 case?
it seems like it should be absurd, but the syntax doens't quite work,

also this is using ulf's agda prelude lib atm, but that shouldn't be
relevant to this question.

Or is this a bug? :)

many thanks
-Carter
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170709/5c868efa/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: SimpleF.agda
Type: application/octet-stream
Size: 1840 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170709/5c868efa/attachment.obj>