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:

  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


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

Page last modified on August 18, 2007, at 11:17 AM
Powered by PmWiki