matita/matita/help/C/html/index.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"><html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>Matita V0.99.5 User Manual (rev. 0.99.5 )</title><link rel="stylesheet" type="text/css" href="docbook.css" /><meta name="generator" content="DocBook XSL Stylesheets Vsnapshot" /><link rel="home" href="index.html" title="Matita V0.99.5 User Manual (rev. 0.99.5 )" /><link rel="next" href="sec_intro.html" title="Chapter 1. Introduction" /></head><body><a xmlns="" href="../../../"><div class="matita_logo"><img src="figures/matita.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"><span class="application">Matita</span> V0.99.5
   3  User Manual (rev. 0.99.5
   4 )</th></tr><tr><td width="20%" align="left"> </td><th width="60%" align="center"> </th><td width="20%" align="right"> <a accesskey="n" href="sec_intro.html">Next</a></td></tr></table><hr /></div><div xml:lang="en" class="book" lang="en"><div class="titlepage"><div><div><h1 class="title"><a id="matita_manual"></a><span class="application">Matita</span> V0.99.5
   5  User Manual (rev. 0.99.5
   6 )</h1></div><div><ul xmlns="" class="authorgroup"><li class="author">Andrea Asperti &lt;<a href="mailto:asperti@cs.unibo.it">asperti@cs.unibo.it</a>&gt;</li><li class="author">Claudio Sacerdoti Coen &lt;<a href="mailto:sacerdot@cs.unibo.it">sacerdot@cs.unibo.it</a>&gt;</li><li class="author">Ferruccio Guidi &lt;<a href="mailto:fguidi@cs.unibo.it">fguidi@cs.unibo.it</a>&gt;</li><li class="author">Enrico Tassi &lt;<a href="mailto:tassi@cs.unibo.it">tassi@cs.unibo.it</a>&gt;</li><li class="author">Stefano Zacchiroli &lt;<a href="mailto:zacchiro@cs.unibo.it">zacchiro@cs.unibo.it</a>&gt;</li></ul></div><div><p class="copyright">Copyright © 2006 The HELM team.</p></div><div><div class="legalnotice"><a id="idm39"></a><p> Both Matita and this document are free software, you can
   7         redistribute them and/or modify them under the terms of the GNU General
   8         Public License as published by the Free Software Foundation.  See <a class="xref" href="sec_license.html" title="Chapter 10. License">Chapter 10, <em>License</em></a> for more information. </p></div></div><div><div xmlns="" class="revhistory"><span class="revision">Revision: <span class="revnumber">0.99.5
   9 </span>, <span class="date">12/07/2006</span></span></div></div></div><hr /></div><div class="toc"><p><strong>Table of Contents</strong></p><dl class="toc"><dt><span class="chapter"><a href="sec_intro.html">1. Introduction</a></span></dt><dd><dl><dt><span class="sect1"><a href="sec_intro.html#Features">Features</a></span></dt><dt><span class="sect1"><a href="WrtCoq.html">Matita vs Coq</a></span></dt></dl></dd><dt><span class="chapter"><a href="sec_install.html">2. Installation</a></span></dt><dd><dl><dt><span class="sect1"><a href="sec_install.html#inst_livecd">Using the LiveCD</a></span></dt><dd><dl><dt><span class="sect2"><a href="sec_install.html#make_vmachine">Creating the virtual machine</a></span></dt><dt><span class="sect2"><a href="sec_install.html#idm148">Sharing files with the real PC</a></span></dt></dl></dd><dt><span class="sect1"><a href="inst_from_src.html">Installing from sources</a></span></dt><dd><dl><dt><span class="sect2"><a href="inst_from_src.html#get_source_code">Getting the source code</a></span></dt><dt><span class="sect2"><a href="inst_from_src.html#build_requirements">Requirements</a></span></dt><dt><span class="sect2"><a href="inst_from_src.html#build_instructions">Compiling and installing</a></span></dt></dl></dd></dl></dd><dt><span class="chapter"><a href="sec_gettingstarted.html">3. Getting started</a></span></dt><dd><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></dl></dd><dt><span class="sect1"><a href="authoring.html">Authoring</a></span></dt><dd><dl><dt><span class="sect2"><a href="authoring.html#compilation">How to compile a script</a></span></dt><dt><span class="sect2"><a href="authoring.html#authoringinterface">The authoring interface</a></span></dt></dl></dd></dl></dd><dt><span class="chapter"><a href="sec_terms.html">4. Syntax</a></span></dt><dd><dl><dt><span class="sect1"><a href="sec_terms.html#terms_and_co">Terms &amp; co.</a></span></dt><dd><dl><dt><span class="sect2"><a href="sec_terms.html#lexical">Lexical conventions</a></span></dt><dt><span class="sect2"><a href="sec_terms.html#terms">Terms</a></span></dt></dl></dd><dt><span class="sect1"><a href="axiom_definition_declaration.html">Definitions and declarations</a></span></dt><dd><dl><dt><span class="sect2"><a href="axiom_definition_declaration.html#axiom">axiom</a></span></dt><dt><span class="sect2"><a href="axiom_definition_declaration.html#definition">definition</a></span></dt><dt><span class="sect2"><a href="axiom_definition_declaration.html#discriminator">discriminator</a></span></dt><dt><span class="sect2"><a href="axiom_definition_declaration.html#inverter">inverter</a></span></dt><dt><span class="sect2"><a href="axiom_definition_declaration.html#letrec"><span class="emphasis"><em>TODO</em></span></a></span></dt><dt><span class="sect2"><a href="axiom_definition_declaration.html#inductive">(co)inductive types declaration</a></span></dt><dt><span class="sect2"><a href="axiom_definition_declaration.html#record">record</a></span></dt></dl></dd><dt><span class="sect1"><a href="proofs.html">Proofs</a></span></dt><dd><dl><dt><span class="sect2"><a href="proofs.html#theorem">theorem</a></span></dt><dt><span class="sect2"><a href="proofs.html#corollary">corollary</a></span></dt><dt><span class="sect2"><a href="proofs.html#lemma">lemma</a></span></dt><dt><span class="sect2"><a href="proofs.html#fact">fact</a></span></dt><dt><span class="sect2"><a href="proofs.html#example">example</a></span></dt></dl></dd><dt><span class="sect1"><a href="tacticargs.html">Tactic arguments</a></span></dt><dd><dl><dt><span class="sect2"><a href="tacticargs.html#pattern">pattern</a></span></dt><dt><span class="sect2"><a href="tacticargs.html#reduction-kind">reduction-kind</a></span></dt><dt><span class="sect2"><a href="tacticargs.html#auto-params">auto-params</a></span></dt><dt><span class="sect2"><a href="tacticargs.html#justification">justification</a></span></dt></dl></dd></dl></dd><dt><span class="chapter"><a href="sec_usernotation.html">5. Extending the syntax</a></span></dt><dd><dl><dt><span class="sect1"><a href="sec_usernotation.html#idm1489">notation</a></span></dt><dt><span class="sect1"><a href="ch05s02.html">interpretation</a></span></dt></dl></dd><dt><span class="chapter"><a href="sec_tacticals.html">6. Tacticals</a></span></dt><dd><dl><dt><span class="sect1"><a href="sec_tacticals.html#idm2224">Interactive proofs and definitions</a></span></dt><dt><span class="sect1"><a href="proofstatus.html">The proof status</a></span></dt><dt><span class="sect1"><a href="tacticals.html">Tacticals</a></span></dt></dl></dd><dt><span class="chapter"><a href="sec_tactics.html">7. Tactics</a></span></dt><dd><dl><dt><span class="sect1"><a href="sec_tactics.html#tactics_quickref">Quick reference card</a></span></dt><dt><span class="sect1"><a href="tac_apply.html">@</a></span></dt><dt><span class="sect1"><a href="tac_auto.html">//</a></span></dt><dt><span class="sect1"><a href="tac_intro.html">#</a></span></dt><dt><span class="sect1"><a href="tac_intro_clear.html">#_</a></span></dt><dt><span class="sect1"><a href="macro_intro.html">##</a></span></dt><dt><span class="sect1"><a href="tac_clear.html">-</a></span></dt><dt><span class="sect1"><a href="tac_constructor.html">%</a></span></dt><dt><span class="sect1"><a href="tac_decompose.html">*</a></span></dt><dt><span class="sect1"><a href="tac_rewrite.html">&gt;</a></span></dt><dt><span class="sect1"><a href="tac_applyS.html">applyS</a></span></dt><dt><span class="sect1"><a href="tac_assumption.html">assumption</a></span></dt><dt><span class="sect1"><a href="tac_cases.html">cases</a></span></dt><dt><span class="sect1"><a href="tac_change.html">change</a></span></dt><dt><span class="sect1"><a href="tac_cut.html">cut</a></span></dt><dt><span class="sect1"><a href="tac_destruct.html">destruct</a></span></dt><dt><span class="sect1"><a href="tac_elim.html">elim</a></span></dt><dt><span class="sect1"><a href="tac_generalize.html">generalize</a></span></dt><dt><span class="sect1"><a href="tac_inversion.html">inversion</a></span></dt><dt><span class="sect1"><a href="tac_lapply.html">lapply</a></span></dt><dt><span class="sect1"><a href="tac_letin.html">letin</a></span></dt><dt><span class="sect1"><a href="tac_normalize.html">normalize</a></span></dt><dt><span class="sect1"><a href="tac_whd.html">whd</a></span></dt></dl></dd><dt><span class="chapter"><a href="sec_declarative_tactics.html">8. Declarative Tactics</a></span></dt><dd><dl><dt><span class="sect1"><a href="sec_declarative_tactics.html#declarative_tactics_quickref">Quick reference card</a></span></dt><dt><span class="sect1"><a href="tac_assume.html">assume</a></span></dt><dt><span class="sect1"><a href="tac_suppose.html">suppose</a></span></dt><dt><span class="sect1"><a href="tac_let.html">letin</a></span></dt><dt><span class="sect1"><a href="tac_thatisequivalentto.html">that is equivalent to</a></span></dt><dt><span class="sect1"><a href="tac_thesisbecomes.html">the thesis becomes</a></span></dt><dt><span class="sect1"><a href="tac_weneedtoprove.html">we need to prove</a></span></dt><dt><span class="sect1"><a href="tac_bytermweproved.html">we proved</a></span></dt><dt><span class="sect1"><a href="tac_existselim.html">let such that</a></span></dt><dt><span class="sect1"><a href="tac_andelim.html">we have</a></span></dt><dt><span class="sect1"><a href="tac_weproceedbyinduction.html">we proceed by induction on</a></span></dt><dt><span class="sect1"><a href="tac_weproceedbycases.html">we proceed by cases on</a></span></dt><dt><span class="sect1"><a href="tac_case.html">case</a></span></dt><dt><span class="sect1"><a href="tac_byinduction.html">by induction hypothesis we know</a></span></dt><dt><span class="sect1"><a href="tac_conclude.html">conclude</a></span></dt><dt><span class="sect1"><a href="tac_obtain.html">obtain</a></span></dt><dt><span class="sect1"><a href="tac_rewrite_step.html">=</a></span></dt><dt><span class="sect1"><a href="tac_bydone.html">done</a></span></dt></dl></dd><dt><span class="chapter"><a href="sec_commands.html">9. Other commands</a></span></dt><dd><dl><dt><span class="sect1"><a href="sec_commands.html#command_alias">alias</a></span></dt><dt><span class="sect1"><a href="command_check.html">check</a></span></dt><dt><span class="sect1"><a href="command_coercion.html">coercion</a></span></dt><dt><span class="sect1"><a href="command_include.html">include</a></span></dt><dt><span class="sect1"><a href="command_include_alias.html">include alias</a></span></dt><dt><span class="sect1"><a href="command_qed.html">qed</a></span></dt><dt><span class="sect1"><a href="command_qed_minus.html">qed-</a></span></dt><dt><span class="sect1"><a href="command_unification_hint.html">unification hint</a></span></dt><dt><span class="sect1"><a href="command_universe_constraints.html">universe constraint</a></span></dt></dl></dd><dt><span class="chapter"><a href="sec_license.html">10. License</a></span></dt></dl></div><div class="list-of-figures"><p><strong>List of Figures</strong></p><dl><dt>2.1. <a href="sec_install.html#idm116">The brand new virtual machine</a></dt><dt>2.2. <a href="sec_install.html#idm124">Mounting an ISO image</a></dt><dt>2.3. <a href="sec_install.html#idm132">Choosing the ISO image</a></dt><dt>2.4. <a href="sec_install.html#idm140">Choosing the ISO image</a></dt><dt>2.5. <a href="sec_install.html#idm153">Set up a shared folder</a></dt><dt>2.6. <a href="sec_install.html#idm161">Choosing the folder to share</a></dt><dt>2.7. <a href="sec_install.html#idm169">Naming the shared folder</a></dt><dt>2.8. <a href="sec_install.html#idm177">Using it from the virtual machine</a></dt></dl></div><div class="list-of-tables"><p><strong>List of Tables</strong></p><dl><dt>4.1. <a href="sec_terms.html#idm389">qstring</a></dt><dt>4.2. <a href="sec_terms.html#idm402">id</a></dt><dt>4.3. <a href="sec_terms.html#idm414">nat</a></dt><dt>4.4. <a href="sec_terms.html#idm426">char</a></dt><dt>4.5. <a href="sec_terms.html#idm440">uri-step</a></dt><dt>4.6. <a href="sec_terms.html#idm454">uri</a></dt><dt>4.7. <a href="sec_terms.html#idm487">csymbol</a></dt><dt>4.8. <a href="sec_terms.html#idm500">symbol</a></dt><dt>4.9. <a href="sec_terms.html#tbl_terms">Terms</a></dt><dt>4.10. <a href="sec_terms.html#idm665">Simple terms</a></dt><dt>4.11. <a href="sec_terms.html#idm792">Arguments</a></dt><dt>4.12. <a href="sec_terms.html#idm870">Pattern matching</a></dt><dt>4.13. <a href="tacticargs.html#idm1235">pattern</a></dt><dt>4.14. <a href="tacticargs.html#idm1275">path</a></dt><dt>4.15. <a href="tacticargs.html#idm1378">reduction-kind</a></dt><dt>4.16. <a href="tacticargs.html#idm1402">auto-params</a></dt><dt>4.17. <a href="tacticargs.html#idm1423">simple-auto-param</a></dt><dt>4.18. <a href="tacticargs.html#idm1466">justification</a></dt><dt>5.1. <a href="sec_usernotation.html#idm1537">usage</a></dt><dt>5.2. <a href="sec_usernotation.html#idm1555">associativity</a></dt><dt>5.3. <a href="sec_usernotation.html#idm1582">notation_rhs</a></dt><dt>5.4. <a href="sec_usernotation.html#idm1604">unparsed_ast</a></dt><dt>5.5. <a href="sec_usernotation.html#idm1639">enriched_term</a></dt><dt>5.6. <a href="sec_usernotation.html#idm1655">unparsed_meta</a></dt><dt>5.7. <a href="sec_usernotation.html#idm1690">level2_meta</a></dt><dt>5.8. <a href="sec_usernotation.html#idm1806">notation_lhs</a></dt><dt>5.9. <a href="sec_usernotation.html#idm1820">layout</a></dt><dt>5.10. <a href="sec_usernotation.html#idm2094">literal</a></dt><dt>5.11. <a href="ch05s02.html#idm2170">interpretation_argument</a></dt><dt>5.12. <a href="ch05s02.html#idm2185">interpretation_rhs</a></dt><dt>6.1. <a href="tacticals.html#idm2266">proof script</a></dt><dt>6.2. <a href="tacticals.html#idm2281">proof steps</a></dt><dt>6.3. <a href="tacticals.html#idm2377">tactics and LCF tacticals</a></dt><dt>7.1. <a href="sec_tactics.html#idm2483">tactics</a></dt><dt>8.1. <a href="sec_declarative_tactics.html#idm3387">tactics</a></dt></dl></div></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"> </td><td width="20%" align="center"> </td><td width="40%" align="right"> <a accesskey="n" href="sec_intro.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top"> </td><td width="20%" align="center"> </td><td width="40%" align="right" valign="top"> Chapter 1. Introduction</td></tr></table></div></body></html>