The Coq mailing list

[Andrea Asperti <asperti AT cs.unibo.it>]

As a first, primitive experiment on the use of
metadata, the HELM on line interface to the coq library

  http://www.cs.unibo.it/helm/library.html

currently support the computation of all objects
containg references to a given object. 
These occurrences are classifed in several groups,
according to the position of the occurrence:

- head position inside the conclusion of a statement
- head position inside an hypothesis of a statement
- other occurrences inside the conclusion
- other occurrences inside an hypothesis
- inside the body

Searching is done on the WHOLE library (the standard
one, PLUS all the main contribs). 

e.g. you may discover that 
        cic:/Coq/Init/Peano/mult.con
occurs in head position inside the conclusion of 96
statements, such as
        
cic:/Algebra/Basics/le_mult_left.con
cic:/Algebra/Basics/lt_mult_right.con
cic:/Algebra/CPoly_Degree/Degree_props/Degree_le_nexp.con
...
and so on.

All the previous uri are obviously hyperlinks to
the corresponding definition (if the list of objects
is reasonably small, the corresponding statements 
are authomatically expanded; otherwise you have 
to follow the link).

In order to view these metadata you must first 
reach the object you are interested in (i.e.
mult, in the above case), and then follow 
the "View its metadata" link in the top frame.

Hope you will have fun (it is quite amusing).
It could be also usefull in view of a possible
restructuration of the "standard" library (and
of course in the development on new contribs).

If you have suggestion and/or comments, please
do not hesitate to contact us.

                        -- andrea asperti
                           & the HELM group