[Agda] how do I handle absurd with patterns?

[Jannis Limperg]

Here's the most direct solution:

  τSubstFancy zero (vτ zero) t | less (diff _ ())

The second argument to `diff`, which we match with the absurd pattern,
is of the form `0 = suc _`. `lt` can't be matched with an absurd pattern
directly because there is a possible (type-correct) choice of
constructor, `diff`.

Of course, you can package this up in a lemma for future reference:

  n<z-absurd : ∀ {i} {A : Set i} {n : Nat} → n < 0 → A
  n<z-absurd (diff x ())

Cheers,
Jannis


On 07/09/2017 06:26 PM, Carter Schonwald wrote:
> 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 --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 858 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170709/519d378d/attachment.sig>