helm/www/matita/docs/manual/sec_gettingstarted.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>Chapter 3. Getting started</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="index.html" title="Matita V0.1.0&#10; User Manual (rev. 1α)" /><link rel="prev" href="sec_install.html" title="Chapter 2. Installation" /><link rel="next" href="cicbrowser.html" title="Browsing and searching" /></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">Chapter 3. Getting started</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="sec_install.html">Prev</a> </td><th width="60%" align="center"> </th><td width="20%" align="right"> <a accesskey="n" href="cicbrowser.html">Next</a></td></tr></table><hr /></div><div class="chapter" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title"><a id="sec_gettingstarted"></a>Chapter 3. Getting started</h2></div></div></div><div class="toc"><p><b>Table of Contents</b></p><dl><dt><span class="sect1"><a href="sec_gettingstarted.html#unicode">How to type Unicode symbols</a></span></dt><dt><span class="sect1"><a href="cicbrowser.html">Browsing and searching</a></span></dt><dd><dl><dt><span class="sect2"><a href="cicbrowser.html#browsinglib">Browsing the library</a></span></dt><dt><span class="sect2"><a href="cicbrowser.html#aboutproof">Looking at a proof under development</a></span></dt><dt><span class="sect2"><a href="cicbrowser.html#whelp">Searching the library</a></span></dt></dl></dd><dt><span class="sect1"><a href="authoring.html">Authoring</a></span></dt><dd><dl><dt><span class="sect2"><a href="authoring.html#developments">How to use developments</a></span></dt></dl></dd></dl></div><p> If you are already familiar with the Calculus of (Co)Inductive
   4   Constructions (CIC) and with interactive theorem provers with procedural
   5   proof languages (expecially Coq), getting started with Matita is relatively
   6   easy. You just need to learn how to type Unicode symbols, how to browse
   7   and search the library and how to author a proof script.</p><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="unicode"></a>How to type Unicode symbols</h2></div></div></div><p>Unicode characters can be typed in several ways:</p><div class="itemizedlist"><ul type="disc"><li><p>Using the "Ctrl+Shift+Unicode code" standard Gnome shortcut. E.g. Ctrl+Shift+3a9 generates "Ω".</p></li><li><p>Typing the ligature "\name" where "name"
   8       is a standard Unicode or LaTeX name for the character. Pressing
   9       "Alt+L" just after the last character of the name converts
  10       the ligature to the Unicode symbol. This operation is
  11       not required since Matita understands also the "\name"
  12       sequences. E.g. "\Omega" followed by Alt+L generates
  13       "Ω".</p></li><li><p>Typing one of the following ligatures (and optionally
  14          converting the ligature to the Unicode character has described before):
  15          ":=" (which stands for ≝); "-&gt;" (which stands for
  16          "→"); "=&gt;" (which stands for "⇒").</p></li></ul></div></div></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="sec_install.html">Prev</a> </td><td width="20%" align="center"> </td><td width="40%" align="right"> <a accesskey="n" href="cicbrowser.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">Chapter 2. Installation </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> Browsing and searching</td></tr></table></div></body></html>