Been playing and, well... it's amazing stuff. Here are the problems
I've run into:
* as constructor declarations,
nil:List Xand (--! are inequivalent, strangely (?)
!nil:List X)
* in
( X : *!( xs : List X ; x : X !
data !-
Hi Jules, hi all,
Good to hear from you. Nice to see that you've tripped over a whole
bunch of issues which arise mostly because things are still a bit
sketchy. So I'm doing what I usually do on this list: apologizing
for the fact that I have no better source of round tuits than anyone
else.
Jules
On Thu, Sep 02, 2004 at 04:38:39PM +0100, Thorsten Altenkirch wrote:
> >
> >Why won't length type check? the 'n' is on a yellow background.
>
> Because there is no n on the left hand side, hence the variable is not
> bound.
Surely there is an n on the left hand side, inside the type of v?
Certai
I have a simpler problem also:
--
( n : Nat !
data (-! where zero : Nat ; !-!
! Nat : * ) ! suc n : Nat )
--
[ah, this majordomo doesn't send you copies of your own emails. That
confused me for a while...]
On Thu, Sep 02, 2004 at 04:05:34PM +0100, Thorsten Altenkirch wrote:
> Jules Bean wrote:
> >Been playing and, well... it's amazing stuff. Here are the problems
> >I've run into:
> >
> >* as constructo
Jules Bean wrote:
Been playing and, well... it's amazing stuff. Here are the problems
I've run into:
* as constructor declarations,
nil:List Xand (--! are inequivalent, strangely (?)
!nil:List X)
nil : List X is not (syntactically) a constructor declaration. The 2nd v
