Re: [mizar] @; and @by

[Adam Naumowicz <adamn@math.uwb.edu.pl>]

Hi Piotr,

On Sun, 6 Feb 2011, Piotr Rudnicki wrote:

> Analogously to @proof, I propose to add to Mizar also a possibility to
> switch-off checking of simple justifications by using @; and @by.
>
> Reason: inside a longer proof I frequently have several places which are on
> the 'frontier' and I do not want them being checked and marked with the *4
> error.
>
> What I do now is add @proof end; in such cases, but I cannot do it in steps
> where proofs are not allowed and then 'contradiction @proof end; then' does
> the trick.
>
> @by is needed for cases where I want to switch-off checking of a
> long-running step.
>
> All this can be done with pragmas.  There was some discussion of pragmas
> some time ago but I do not see any documentation/info about it.

Yes, you can now do it with pragmas. Here is a list of implemented pragmas 
which change the way the verifier processes an article:

::$V-
(do not call the checker from now on)
::$V+
(restore calling the checker in a standard way)
::$P-
(ignore proofs from now on, may be used instead of @proof)
::$P+
(restore checking proofs in a standard way)
::$S-
(do not call the schematizer from now on)
::$S+
(restore calling the schematizer in a standard way)
::$EOF
(works as a virtual end of file)

Please note that lexically the pragmas are treated as comments, and they 
carry their special meaning only if they are placed at the beginning of a 
line.

Best,

Adam

=======================================================================
Dept. of Programming and Formal Methods  Fax: +48(85)7457662
Institute of Informatics                 Tel: +48(85)7457559 (office)
University of Bialystok                  E-mail: adamn@mizar.org
Sosnowa 64, 15-887 Bialystok, Poland     http://math.uwb.edu.pl/~adamn/
=======================================================================