[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
[mizar] 'Environmental' problems
- To: mizar-forum@mizar.uwb.edu.pl
- Subject: [mizar] 'Environmental' problems
- From: Борис Шминке <schminkeba@gmail.com>
- Date: Wed, 31 Mar 2010 08:28:33 +0400
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type; b=gFDQh29pWtNzy31/SNL9WIcdWqV8BqtRPjBDZzjuXy9KCvTVNyTasQG65C3sRPcLa1 x5cjn2L1+N7goij3M+/S0JbobHiDf59IhPfal+U/YZ8nDOGwByPpXDMXv3CzoDuLHwUw pFKT/bWcC9nvUO4GmlswxM5JEbyuyGO7HW00Y=
Dear all,
I'm only a stupid newbie and it was hard for me even to start using
this forum, but I have a question. Yes, unfortunately to all
experienced users of Mizar System, the question is about environment
section of an article. I've read the advises to copy it from some
article on the relevant theme, but I still want to understand how it
works.
So, what I have:
environ
vocabularies ARYTM_3, NAT_1;
notations ARYTM_3, NAT_1;
constructors ARYTM_3, NAT_1;
registrations NAT_1;
begin
reserve x, y for Nat;
theorem x + y = x + y
::> *103 *103
proof
end;
::> 103: Unknown functor
I've added 'registrations NAT_1' line because there is a cluster:
registration
let n,k be Nat;
cluster n + k -> natural;
end;
in NAT_1. So I expected, that it would be enough, but it wasn't.
Could you explain me, why the functor '+' is still unknown? How to
correct the situation and why it will be correct?
Regards,
Boris Schminke.