Browsing and searching

The CIC browser is used to browse and search the library. You can open a new CIC browser selecting "New Cic Browser" from the "View" menu of Matita, or by pressing "F3". The CIC browser is similar to a traditional Web browser.

Browsing the library

To browse the library, type in the location bar the absolute URI of the theorem, definition or library fragment you are interested in. "cic:/" is the root of the library. Contributions developed in Matita are under "cic:/matita"; all the others are part of the library of Coq.

Following the hyperlinks it is possible to navigate in the Web of mathematical notions. Proof are rendered in pseudo-natural language and mathematical notation is used for formulae. For now, mathematical notation must be included in the current script to be activated, but we plan to remove this limitation.

Looking at a proof under development

A proof under development is not yet part of the library. The special URI "about:proof" can be used to browse the proof currently under development, if there is one. The "home" button of the CIC browser sets the location bar to "about:proof".

Searching the library

The query bar of the CIC browser can be used to search the library of Matita for theorems or definitions that match certain criteria. The criteria is given by typing a term in the query bar and selecting an action in the drop down menu right of it.

Searching by name


List of lemmas that can be applied


Searching by exact match


List of elimination principles for a given type


Searching by instantiation