20070808-1

The use of a@ in this code fragment

  accSucc : (x : Nat) -> Acc Nat Lt x -> Acc Nat Lt (succ x)
  accSucc x a@(acc .x h) = acc (succ x) (\ y p -> ltcase y x p (Acc Nat Lt) h a)

causes a Panic:

  BUG-THINGOUTOFCXT.agda:26,77-78
  Panic: thing out of context ([CtxId 147,CtxId 146] not prefix of
  [CtxId 149,CtxId 148,CtxId 147,CtxId 146])
  when checking that the expression a has type Acc Nat Lt x

Attach:Bug.agda

@-patterns are currently very much broken. Don't use them. -Ulf