Error Messages

[sualitu]

Post Error Messages.

[sualitu]

When using unknown projections such as:

corecord Stream' : Type -> Type where
  hd : Stream' a -> a
  tl : Stream' b -> Stream' a
  constructor (::)

zeros : Stream' Nat
&hd zeros = Z
&til zeros = zeros

You get the following error message:

No type declaration for til

This should be something along the lines projection not found (possibly for type). If we're crazy, come up with suggestions.