[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] Mizar 7.7.01 MML 4.68.942
On Fri, Jul 14, 2006 at 02:14:05AM +0200, Adam Grabowski wrote:
> On Thu, 13 Jul 2006, Piotr Rudnicki wrote:
>
> >What am I supposed to do now to make
> >
> > natural number
> >
> >behave as
> >
> > element of NAT
> >
> >without reconsidering or something equally bad?
> The solution is probably to avoid the latter 'Element of NAT'
> in the Mizar source because as of now, reconsidering is necessary.
> So authors are strongly encouraged to use 'Nat' or 'natural number'
> in their submissions.
Any suggestions on how to use functors from MML that require Element of NAT?
Would this be the right opportunity to revise MML? The offender for me
is -cut from GRAPH_2.
> >
> >Also, how does the verifier know that Element of NAT is natural?
> >I cannot find a cluster to this effect.
> The point is that 'NAT' is synonymic to 'omega' - and ARYTM_3 contains
> appropriate conditional cluster registration.
Thanks. I have discovered it many times in the past on my own
and will probably ask the same question many times in the future ;-)
Cheers,
--
Piotr Rudnicki CompSci, University of Alberta, Edmonton, Canada
http://web.cs.ualberta.ca/~piotr