helm/software/matita/help/C/sec_gettingstarted.xml

   1
   2 <!-- ============= Getting started ============================== -->
   3
   4 <chapter id="sec_gettingstarted">
   5   <title>Getting started</title>
   6   <para> If you are already familiar with the Calculus of (co)Inductive
   7   Constructions (CIC) and with interactive theorem provers with procedural
   8   proof languages (expecially Coq), getting started with Matita is relatively
   9   easy. You just need to learn how to type Unicode symbols, how to browse
  10   and search the library and how to author a proof script.</para>
  11
  12   <sect1 id="unicode">
  13    <title>How to type Unicode symbols</title>
  14    Unicode characters can be typed in several ways:
  15     <itemizedlist>
  16      <listitem>Using the &quot;Shift+Ctrl+Unicode code&quot; standard
  17       Gnome shortcut. E.g. Shift+Ctrl+3a9 generates &quot;Ω&quot;.
  18      </listitem>
  19      <listitem>Typing the ligature &quot;\name&quot; where &quot;name&quot;
  20       is a standard Unicode or LaTeX name for the character. Pressing
  21       &quot;Alt+L&quot; just after the last character of the name converts
  22       the ligature to the Unicode symbol. This operation is
  23       not required since Matita understands also the &quot;\name&quot;
  24       sequences. E.g. &quot;\Omega&quot; followed by Alt+L generates
  25       &quot;Ω&quot;.
  26      </listitem>
  27      <listitem>Typing one of the following ligatures (and opzionally converting
  28       the ligature to the Unicode character has described before):
  29       &quot;:=&quot; (which stands for ≝); &quot;->&quot; (which stands for &quot;→&quot;);
  30       &quot;->&quot; (which stands for &quot;⇒&quot;).
  31      </listitem>
  32     </itemizedlist>
  33   </sect1>
  34   <sect1 id="cicbrowser">
  35    <title>Browsing and searching</title>
  36    <para>The CIC browser is used to browse and search the library.
  37     You can open a new CIC browser selecting &quot;New Cic Browser&quot;
  38     from the &quot;View&quot; menu of Matita, or by pressing &quot;F3&quot;.
  39     The CIC browser is similar to a traditional Web browser.</para>
  40    <sect2 id="browsinglib">
  41     <title>Browsing the library</title>
  42     <para>To browse the library, type in the location bar the absolute URI of
  43     the theorem, definition or library fragment you are interested in.
  44     &quot;cic:/&quot; is the root of the library. Contributions developed
  45     in Matita are under &quot;cic:/matita&quot;; all the others are
  46     part of the library of Coq.</para>
  47     <para>Following the hyperlinks it is possible to navigate in the Web
  48     of mathematical notions. Proof are rendered in pseudo-natural language
  49     and mathematical notation is used for formulae. For now, mathematical
  50     notation must be included in the current script to be activated, but we
  51     plan to remove this limitation.</para>
  52    </sect2>
  53    <sect2 id="aboutproof">
  54     <title>Looking at a proof under development</title>
  55     <para>A proof under development is not yet part of the library.
  56      The special URI &quot;about:proof&quot; can be used to browse the
  57      proof currently under development, if there is one.
  58      The &quot;home&quot; button of the CIC browser sets the location bar to
  59      &quot;about:proof&quot;.
  60     </para>
  61    </sect2>
  62    <sect2 id="whelp">
  63     <title>Searching the library</title>
  64     <para>The query bar of the CIC browser can be used to search the library
  65      of Matita for theorems or definitions that match certain criteria.
  66      The criteria is given by typing a term in the query bar and selecting
  67      an action in the drop down menu right of it.</para>
  68     <sect3 id="locate">
  69      <title>Searching by name</title>
  70      &TODO;
  71     </sect3>
  72     <sect3 id="hint">
  73      <title>List of lemmas that can be applied</title>
  74      &TODO;
  75     </sect3>
  76     <sect3 id="match">
  77      <title>Searching by exact match</title>
  78      &TODO;
  79     </sect3>
  80     <sect3 id="elim">
  81      <title>List of elimination principles for a given type</title>
  82      &TODO;
  83     </sect3>
  84     <sect3 id="instance">
  85      <title>Searching by instantiation</title>
  86      &TODO;
  87     </sect3>
  88    </sect2>
  89   </sect1>
  90   <sect1 id="authoring">
  91    <title>Authoring</title>
  92    &TODO;
  93   </sect1>
  94 </chapter>
  95