[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] Re: a term representing the extension of a type
Hi Jesse,
On Wed, 27 Dec 2006, Jesse Alama wrote:
How can I determine where in, say, FINSET_1, the registration
FINSET_1:exreg 1 occurs, whether there even is such a thing?
Couple of ways:
- http://mmlquery.mizar.org/mml/current/finset_1.html#RC1
here RC, FC, and CC stand for registration (existential), functor (term),
and conditional clusters (registrations) (btw. the terminology is a bit
wild now :-).
- the MML Query abstracts:
http://mmlquery.mizar.org/mmlquery/gab/4.75.958/finset_1.html#FINSET_1:exreg.1
- in Emacs, look at the Index menu for the finset_1.abs or finset_1.abs
buffer, there should be something called "Registrations" there
Determining whether there even is such a thing is harder, most people just
grep abstracts for "cluster" (C-c g in Emacs) possibly with a symbol that
should appear there. MML Query is more semantical and all the symbols are
linked to their definitions there.
Is there a command line tool for finding out the answers to these
questions?
Well, grep :-). The closest approximation would be MML Query installed
locally, I think Grzegorz used to have a "shell mode" there (we even did
some trivial integration with Emacs). One cheap "command line"
querying tool could eventually also be just libxml used e.g. inside Perl
(see
http://kti.ms.mff.cuni.cz/cgi-bin/viewcvs.cgi/mizarmode/Consider.pl?view=markup
for an example) run over the xml database in the "prel" directory. But for
simple notational queries the xml encoding of "prel"s would have to be
made a bit more explicit. In a way, the "constr" utility is a limited
version of such a tool, and unlike libxml it comes with Mizar :-).
Also, there are a bunch of applications like constr that are
distributed with mizar. Where can I find documentation for these?
I would check the manuals at http://mizar.org/project/bibliography.html,
especially Freek's tutorial and perhaps also the "Mizar Lecture Notes".
Best,
Josef