'Environmental' problems
Борис Шминке <[email protected]>
| Newsgroups | gmane.comp.mathematics.mizar |
|---|---|
| Message-ID | <[email protected]> |
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.