helm/www/matita/docs/manual/cicbrowser.html

   1 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
   2 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
   3 <html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>Browsing and searching</title><link rel="stylesheet" href="docbook.css" type="text/css" /><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0&#10; User Manual (rev. 1α)" /><link rel="up" href="sec_gettingstarted.html" title="Chapter 3. Getting started" /><link rel="prev" href="sec_gettingstarted.html" title="Chapter 3. Getting started" /><link rel="next" href="authoring.html" title="Authoring" /></head><body><a xmlns="" href="../../"><div class="matita_logo"><img src="../../images/matita-tiny.png" alt="Tiny Matita logo" /><span>Matita Home</span></div></a><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">Browsing and searching</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="sec_gettingstarted.html">Prev</a> </td><th width="60%" align="center">Chapter 3. Getting started</th><td width="20%" align="right"> <a accesskey="n" href="authoring.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="cicbrowser"></a>Browsing and searching</h2></div></div></div><p>The CIC browser is used to browse and search the library.
   4     You can open a new CIC browser selecting "New Cic Browser"
   5     from the "View" menu of Matita, or by pressing "F3".
   6     The CIC browser is similar to a traditional Web browser.</p><div class="sect2" lang="en" xml:lang="en"><div class="titlepage"><div><div><h3 class="title"><a id="browsinglib"></a>Browsing the library</h3></div></div></div><p>To browse the library, type in the location bar the absolute URI of
   7     the theorem, definition or library fragment you are interested in.
   8     "cic:/" is the root of the library. Contributions developed
   9     in Matita are under "cic:/matita"; all the others are
  10     part of the library of Coq.</p><p>Following the hyperlinks it is possible to navigate in the Web
  11     of mathematical notions. Proof are rendered in pseudo-natural language
  12     and mathematical notation is used for formulae. For now, mathematical
  13     notation must be included in the current script to be activated, but we
  14     plan to remove this limitation.</p></div><div class="sect2" lang="en" xml:lang="en"><div class="titlepage"><div><div><h3 class="title"><a id="aboutproof"></a>Looking at a proof under development</h3></div></div></div><p>A proof under development is not yet part of the library.
  15      The special URI "about:proof" can be used to browse the
  16      proof currently under development, if there is one.
  17      The "home" button of the CIC browser sets the location bar to
  18      "about:proof".
  19     </p></div><div class="sect2" lang="en" xml:lang="en"><div class="titlepage"><div><div><h3 class="title"><a id="whelp"></a>Searching the library</h3></div></div></div><p>The query bar of the CIC browser can be used to search the library
  20      of Matita for theorems or definitions that match certain criteria.
  21      The criteria is given by typing a term in the query bar and selecting
  22      an action in the drop down menu right of it.</p><div class="sect3" lang="en" xml:lang="en"><div class="titlepage"><div><div><h4 class="title"><a id="locate"></a>Searching by name</h4></div></div></div><p>     <span class="emphasis"><em>TODO</em></span></p></div><div class="sect3" lang="en" xml:lang="en"><div class="titlepage"><div><div><h4 class="title"><a id="hint"></a>List of lemmas that can be applied</h4></div></div></div><p>     <span class="emphasis"><em>TODO</em></span></p></div><div class="sect3" lang="en" xml:lang="en"><div class="titlepage"><div><div><h4 class="title"><a id="match"></a>Searching by exact match</h4></div></div></div><p>     <span class="emphasis"><em>TODO</em></span></p></div><div class="sect3" lang="en" xml:lang="en"><div class="titlepage"><div><div><h4 class="title"><a id="elim"></a>List of elimination principles for a given type</h4></div></div></div><p>     <span class="emphasis"><em>TODO</em></span></p></div><div class="sect3" lang="en" xml:lang="en"><div class="titlepage"><div><div><h4 class="title"><a id="instance"></a>Searching by instantiation</h4></div></div></div><p>     <span class="emphasis"><em>TODO</em></span></p></div></div></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="sec_gettingstarted.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_gettingstarted.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="authoring.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">Chapter 3. Getting started </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> Authoring</td></tr></table></div></body></html>