[Date Prev][Date Next] [Chronological] [Thread] [Top]

[mizar] 'Environmental' problems



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.