<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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 vs Coq</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_intro.html" title="Chapter 1. Introduction" /><link rel="prev" href="sec_intro.html" title="Chapter 1. Introduction" /><link rel="next" href="sec_install.html" title="Chapter 2. Installation" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">Matita vs Coq</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="sec_intro.html">Prev</a> </td><th width="60%" align="center">Chapter 1. Introduction</th><td width="20%" align="right"> <a accesskey="n" href="sec_install.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="WrtCoq"></a>Matita vs Coq</h2></div></div></div><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>Matita vs Coq</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 User Manual (rev. 1α)" /><link rel="up" href="sec_intro.html" title="Chapter 1. Introduction" /><link rel="prev" href="sec_intro.html" title="Chapter 1. Introduction" /><link rel="next" href="sec_install.html" title="Chapter 2. Installation" /></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">Matita vs Coq</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="sec_intro.html">Prev</a> </td><th width="60%" align="center">Chapter 1. Introduction</th><td width="20%" align="right"> <a accesskey="n" href="sec_install.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="WrtCoq"></a>Matita vs Coq</h2></div></div></div><p>
The system shares a common look&feel with the Coq proof assistant
and its graphical user interface. The two systems have the same logic,
very close proof languages and similar sets of tactics. Moreover,
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>Authoring</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_gettingstarted.html" title="Chapter 3. Getting started" /><link rel="prev" href="cicbrowser.html" title="Browsing and searching" /><link rel="next" href="sec_terms.html" title="Chapter 4. Syntax" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">Authoring</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="cicbrowser.html">Prev</a> </td><th width="60%" align="center">Chapter 3. Getting started</th><td width="20%" align="right"> <a accesskey="n" href="sec_terms.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="authoring"></a>Authoring</h2></div></div></div><div class="sect2" lang="en" xml:lang="en"><div class="titlepage"><div><div><h3 class="title"><a id="developments"></a>How to use developments</h3></div></div></div><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>Authoring</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 User Manual (rev. 1α)" /><link rel="up" href="sec_gettingstarted.html" title="Chapter 3. Getting started" /><link rel="prev" href="cicbrowser.html" title="Browsing and searching" /><link rel="next" href="sec_terms.html" title="Chapter 4. Syntax" /></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">Authoring</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="cicbrowser.html">Prev</a> </td><th width="60%" align="center">Chapter 3. Getting started</th><td width="20%" align="right"> <a accesskey="n" href="sec_terms.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="authoring"></a>Authoring</h2></div></div></div><div class="sect2" lang="en" xml:lang="en"><div class="titlepage"><div><div><h3 class="title"><a id="developments"></a>How to use developments</h3></div></div></div><p>
A development is a set of scripts files that are strictly related (i.e.
they depend on each other). Matita is able to automatically manage
dependencies among the scripts in a development, compiling them in the
</p><p>
The "Developments..." item the File menu (or pressing
Ctrl+D) opens the Developments window.
- </p><div class="figure"><a id="id252
0494"></a><p class="title"><b>Figure 3.1. The Developments window</b></p><div class="mediaobject" align="center"><img src="developments.png" align="middle" alt="Screenshot of the Developments window." /></div></div><p>
+ </p><div class="figure"><a id="id252
1185"></a><p class="title"><b>Figure 3.1. The Developments window</b></p><div class="mediaobject" align="center"><img src="developments.png" align="middle" alt="Screenshot of the Developments window." /></div></div><p>
</p><div class="variablelist"><p class="title"><b>Developments window buttons</b></p><dl><dt><span class="term"><code class="filename">New</code></span></dt><dd><p>
- To create a new Development the user needs to specify a name<sup>[<a id="id2520538" href="#ftn.id2520538">1</a>]</sup>
+ To create a new Development the user needs to specify a name<sup>[<a id="id2521230" href="#ftn.id2521230">1</a>]</sup>
and the root directory in which all scripts will be placed,
eventually organized in subdirectories. The Development should be
named as the directory in which it lives. A "makefile"
</p></dd><dt><span class="term"><code class="filename">Close</code></span></dt><dd><p>
Closes the Developments window
</p></dd></dl></div><p>
- </p></div><div class="footnotes"><br /><hr width="100" align="left" /><div class="footnote"><p><sup>[<a id="ftn.id2520538" href="#id2520538">1</a>] </sup>
+ </p></div><div class="footnotes"><br /><hr width="100" align="left" /><div class="footnote"><p><sup>[<a id="ftn.id2521230" href="#id2521230">1</a>] </sup>
The name of the Development should be the name of the directory in
which it lives. This is not a requirement, but the makefile
automatically generated by matita in the root directory of the
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>Definitions and declarations</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_terms.html" title="Chapter 4. Syntax" /><link rel="prev" href="sec_terms.html" title="Chapter 4. Syntax" /><link rel="next" href="proofs.html" title="Proofs" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">Definitions and declarations</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="sec_terms.html">Prev</a> </td><th width="60%" align="center">Chapter 4. Syntax</th><td width="20%" align="right"> <a accesskey="n" href="proofs.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="axiom_definition_declaration"></a>Definitions and declarations</h2></div></div></div><div class="sect2" lang="en" xml:lang="en"><div class="titlepage"><div><div><h3 class="title"><a id="axiom"></a><span class="bold"><strong>axiom</strong></span> <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span><span class="bold"><strong>:</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span></h3></div></div></div><p><strong class="userinput"><code>axiom H: P</code></strong></p><p><span><strong class="command">H</strong></span> is declared as an axiom that states <span><strong class="command">P</strong></span></p></div><div class="sect2" lang="en" xml:lang="en"><div class="titlepage"><div><div><h3 class="title"><a id="definition"></a><span class="bold"><strong>definition</strong></span> <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>[<span class="bold"><strong>:</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>] [<span class="bold"><strong>≝</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>]</h3></div></div></div><p><strong class="userinput"><code>definition f: T ≝ t</code></strong></p><p><span><strong class="command">f</strong></span> is defined as <span><strong class="command">t</strong></span>;
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>Definitions and declarations</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 User Manual (rev. 1α)" /><link rel="up" href="sec_terms.html" title="Chapter 4. Syntax" /><link rel="prev" href="sec_terms.html" title="Chapter 4. Syntax" /><link rel="next" href="proofs.html" title="Proofs" /></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">Definitions and declarations</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="sec_terms.html">Prev</a> </td><th width="60%" align="center">Chapter 4. Syntax</th><td width="20%" align="right"> <a accesskey="n" href="proofs.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="axiom_definition_declaration"></a>Definitions and declarations</h2></div></div></div><div class="sect2" lang="en" xml:lang="en"><div class="titlepage"><div><div><h3 class="title"><a id="axiom"></a><span class="bold"><strong>axiom</strong></span> <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span><span class="bold"><strong>:</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span></h3></div></div></div><p><strong class="userinput"><code>axiom H: P</code></strong></p><p><span><strong class="command">H</strong></span> is declared as an axiom that states <span><strong class="command">P</strong></span></p></div><div class="sect2" lang="en" xml:lang="en"><div class="titlepage"><div><div><h3 class="title"><a id="definition"></a><span class="bold"><strong>definition</strong></span> <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>[<span class="bold"><strong>:</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>] [<span class="bold"><strong>≝</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>]</h3></div></div></div><p><strong class="userinput"><code>definition f: T ≝ t</code></strong></p><p><span><strong class="command">f</strong></span> is defined as <span><strong class="command">t</strong></span>;
<span><strong class="command">T</strong></span> is its type. An error is raised if the type of
<span><strong class="command">t</strong></span> is not convertible to <span><strong class="command">T</strong></span>.</p><p><span><strong class="command">T</strong></span> is inferred from <span><strong class="command">t</strong></span> if
omitted.</p><p><span><strong class="command">t</strong></span> can be omitted only if <span><strong class="command">T</strong></span> is
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>Browsing and searching</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><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><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.
+<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 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.
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.</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
--- /dev/null
+
+body {
+ background: url(../../images/sheetbg.png);
+}
+
+ul.authorgroup {
+ list-style-type: none;
+ padding-left: 1em;
+}
+
+div.titlepage {
+ background: #eaeaea;
+}
+
+div.titlepage hr {
+ display: none;
+}
+
+div.navheader hr {
+ display: none;
+}
+
+div.navfooter hr {
+ display: none;
+}
+
+div.navheader {
+ padding-left: 150px;
+ background: #eaeaea;
+}
+
+div.navfooter {
+ background: #eaeaea;
+}
+
+div.matita_logo {
+ position: absolute;
+ top: 3px;
+ left: 5px;
+}
+
+div.matita_logo img {
+ border-style: none;
+}
+
+div.matita_logo span {
+ position: absolute;
+ top: 13px;
+ left: 65px;
+ text-decoration: underline;
+}
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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.1.0
- Manual (rev. 0)</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="next" href="sec_intro.html" title="Chapter 1. Introduction" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center"><span class="application">Matita</span> V0.1.0
- Manual (rev. 0)</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 class="book" lang="en" xml:lang="en"><div class="titlepage"><div><div><h1 class="title"><a id="matita_manual"></a><span class="application">Matita</span> V0.1.0
- Manual (rev. 0)</h1></div><div><div class="authorgroup"><div class="author"><h3 class="author"><span class="firstname">Andrea</span> <span class="surname">Asperti</span></h3><div class="affiliation"><div class="address"><p> <code class="email"><<a href="mailto:asperti@cs.unibo.it">asperti@cs.unibo.it</a>></code> </p></div></div></div><div class="author"><h3 class="author"><span class="firstname">Claudio</span> <span class="surname">Sacerdoti Coen</span></h3><div class="affiliation"><div class="address"><p> <code class="email"><<a href="mailto:sacerdot@cs.unibo.it">sacerdot@cs.unibo.it</a>></code> </p></div></div></div><div class="author"><h3 class="author"><span class="firstname">Enrico</span> <span class="surname">Tassi</span></h3><div class="affiliation"><div class="address"><p> <code class="email"><<a href="mailto:tassi@cs.unibo.it">tassi@cs.unibo.it</a>></code> </p></div></div></div><div class="author"><h3 class="author"><span class="firstname">Stefano</span> <span class="surname">Zacchiroli</span></h3><div class="affiliation"><div class="address"><p> <code class="email"><<a href="mailto:zacchiro@cs.unibo.it">zacchiro@cs.unibo.it</a>></code> </p></div></div></div></div></div><div><p class="releaseinfo">This manual describes version 0.1.0
- of Matita.
- </p></div><div><p class="copyright">Copyright © 2006 The HELM team.</p></div><div><div class="legalnotice"><a id="id2472240"></a><p> This file is part of HELM, an Hypertextual, Electronic Library of
- Mathematics, developed at the Computer Science Department, University of
- Bologna, Italy. </p><p> HELM is free software; you can redistribute it and/or modify it under
- the terms of the GNU General Public License as published by the Free
- Software Foundation; either version 2 of the License, or (at your option)
- any later version. </p><p> HELM is distributed in the hope that it will be useful, but WITHOUT
- ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
- FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for
- more details. </p><p> You should have received a copy of the GNU General Public License
- along with HELM; if not, write to the Free Software Foundation, Inc., 59
- Temple Place - Suite 330, Boston, MA 02111-1307, USA. A copy of the GNU
- General Public License is available at <a href="ghelp:gpl" target="_top">this link</a>. </p></div></div><div><div class="legalnotice"><a id="id2472567"></a><p class="legalnotice-title"><b>Feedback</b></p><p>To report a bug or make a suggestion regarding the <span class="application">Matita</span>
- application or this manual, follow the directions in the
- <a href="http://bugs.mowgli.cs.unibo.it" target="_top">HELM Bug
- Tracking System Page</a>.
- </p></div></div><div><div class="revhistory"><table border="1" width="100%" summary="Revision history"><tr><th align="left" valign="top" colspan="3"><b>Revision History</b></th></tr><tr><td align="left">Revision Matita V0.1.0
- Manual (rev. 0)</td><td align="left">February 2006</td><td> </td></tr><tr><td align="left" colspan="3">
- <p class="author">The HELM team
-
- </p>
-
- </td></tr><tr><td align="left">Revision 0</td><td align="left">4 February 2006</td><td align="left">HELM</td></tr><tr><td align="left" colspan="3">
- First draft completed.
- </td></tr></table></div></div></div><hr /></div><div class="toc"><p><b>Table of Contents</b></p><dl><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_from_src">Installing from sources</a></span></dt><dd><dl><dt><span class="sect2"><a href="sec_install.html#get_source_code">Getting the source code</a></span></dt><dt><span class="sect2"><a href="sec_install.html#build_requirements">Requirements</a></span></dt><dt><span class="sect2"><a href="sec_install.html#database_setup">Database setup</a></span></dt><dt><span class="sect2"><a href="sec_install.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><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></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 & 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#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#variant">variant</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#remark">remark</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#id2526491">Introduction</a></span></dt></dl></dd><dt><span class="chapter"><a href="sec_tactics.html">6. Tactics</a></span></dt><dd><dl><dt><span class="sect1"><a href="sec_tactics.html#tac_absurd">absurd</a></span></dt><dt><span class="sect1"><a href="tac_apply.html">apply</a></span></dt><dt><span class="sect1"><a href="tac_assumption.html">assumption</a></span></dt><dt><span class="sect1"><a href="tac_auto.html">auto</a></span></dt><dt><span class="sect1"><a href="tac_clear.html">clear</a></span></dt><dt><span class="sect1"><a href="tac_clearbody.html">clearbody</a></span></dt><dt><span class="sect1"><a href="tac_change.html">change</a></span></dt><dt><span class="sect1"><a href="tac_constructor.html">constructor</a></span></dt><dt><span class="sect1"><a href="tac_contradiction.html">contradiction</a></span></dt><dt><span class="sect1"><a href="tac_cut.html">cut</a></span></dt><dt><span class="sect1"><a href="tac_decompose.html">decompose</a></span></dt><dt><span class="sect1"><a href="tac_discriminate.html">discriminate</a></span></dt><dt><span class="sect1"><a href="tac_elim.html">elim</a></span></dt><dt><span class="sect1"><a href="tac_elimType.html">elimType</a></span></dt><dt><span class="sect1"><a href="tac_exact.html">exact</a></span></dt><dt><span class="sect1"><a href="tac_exists.html">exists</a></span></dt><dt><span class="sect1"><a href="tac_fail.html">failt</a></span></dt><dt><span class="sect1"><a href="tac_fold.html">fold</a></span></dt><dt><span class="sect1"><a href="tac_fourier.html">fourier</a></span></dt><dt><span class="sect1"><a href="tac_fwd.html">fwd</a></span></dt><dt><span class="sect1"><a href="tac_generalize.html">generalize</a></span></dt><dt><span class="sect1"><a href="tac_id.html">id</a></span></dt><dt><span class="sect1"><a href="tac_injection.html">injection</a></span></dt><dt><span class="sect1"><a href="tac_intro.html">intro</a></span></dt><dt><span class="sect1"><a href="tac_intros.html">intros</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_left.html">left</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_paramodulation.html">paramodulation</a></span></dt><dt><span class="sect1"><a href="tac_reduce.html">reduce</a></span></dt><dt><span class="sect1"><a href="tac_reflexivity.html">reflexivity</a></span></dt><dt><span class="sect1"><a href="tac_replace.html">change</a></span></dt><dt><span class="sect1"><a href="tac_rewrite.html">rewrite</a></span></dt><dt><span class="sect1"><a href="tac_right.html">right</a></span></dt><dt><span class="sect1"><a href="tac_ring.html">ring</a></span></dt><dt><span class="sect1"><a href="tac_simplify.html">simplify</a></span></dt><dt><span class="sect1"><a href="tac_split.html">split</a></span></dt><dt><span class="sect1"><a href="tac_symmetry.html">symmetry</a></span></dt><dt><span class="sect1"><a href="tac_transitivity.html">transitivity</a></span></dt><dt><span class="sect1"><a href="tac_unfold.html">unfold</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_tacticals.html">7. Tacticals</a></span></dt><dd><dl><dt><span class="sect1"><a href="sec_tacticals.html#id2534769">Introduction</a></span></dt></dl></dd><dt><span class="chapter"><a href="sec_commands.html">8. Other commands</a></span></dt><dd><dl><dt><span class="sect1"><a href="sec_commands.html#id2535309">Introduction</a></span></dt></dl></dd><dt><span class="chapter"><a href="sec_license.html">9. License</a></span></dt></dl></div><div class="list-of-figures"><p><b>List of Figures</b></p><dl><dt>3.1. <a href="authoring.html#id2520494">The Developments window</a></dt></dl></div><div class="list-of-tables"><p><b>List of Tables</b></p><dl><dt>2.1. <a href="sec_install.html#id2518871"> <span class="application">configure</span> command line
- arguments</a></dt><dt>4.1. <a href="sec_terms.html#id2521399">id</a></dt><dt>4.2. <a href="sec_terms.html#id2521488">nat</a></dt><dt>4.3. <a href="sec_terms.html#id2521498">uri</a></dt><dt>4.4. <a href="sec_terms.html#id2521554">Terms</a></dt><dt>4.5. <a href="sec_terms.html#id2522106">Simple terms</a></dt><dt>4.6. <a href="sec_terms.html#id2522561">Arguments</a></dt><dt>4.7. <a href="sec_terms.html#id2522763">Miscellaneous arguments</a></dt><dt>4.8. <a href="sec_terms.html#id2522867">Pattern matching</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>
+ User Manual (rev. 1α)</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 User Manual (rev. 1α)" /><link rel="next" href="sec_intro.html" title="Chapter 1. Introduction" /></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"><span class="application">Matita</span> V0.1.0
+ User Manual (rev. 1α)</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 class="book" lang="en" xml:lang="en"><div class="titlepage"><div><div><h1 class="title"><a id="matita_manual"></a><span class="application">Matita</span> V0.1.0
+ User Manual (rev. 1α)</h1></div><div><ul xmlns="" class="authorgroup"><li class="author">Andrea Asperti <<a href="mailto:asperti@cs.unibo.it">asperti@cs.unibo.it</a>></li><li class="author">Claudio Sacerdoti Coen <<a href="mailto:sacerdot@cs.unibo.it">sacerdot@cs.unibo.it</a>></li><li class="author">Enrico Tassi <<a href="mailto:tassi@cs.unibo.it">tassi@cs.unibo.it</a>></li><li class="author">Stefano Zacchiroli <<a href="mailto:zacchiro@cs.unibo.it">zacchiro@cs.unibo.it</a>></li></ul></div><div><p class="copyright">Copyright © 2006 The HELM team.</p></div><div><div class="legalnotice"><a id="id2509491"></a><p> Both Matita and this document are free software, you can
+ redistribute them and/or modify them under the terms of the GNU General
+ Public License as published by the Free Software Foundation. See <a href="sec_license.html" title="Chapter 9. License">Chapter 9, <i>License</i></a> for more information. </p></div></div><div><div xmlns="" class="revhistory"><span class="revision">Revision: <span class="revnumber">1α</span>, <span class="date">10/06/2006</span></span></div></div></div><hr /></div><div class="toc"><p><b>Table of Contents</b></p><dl><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_from_src">Installing from sources</a></span></dt><dd><dl><dt><span class="sect2"><a href="sec_install.html#get_source_code">Getting the source code</a></span></dt><dt><span class="sect2"><a href="sec_install.html#build_requirements">Requirements</a></span></dt><dt><span class="sect2"><a href="sec_install.html#database_setup">Database setup</a></span></dt><dt><span class="sect2"><a href="sec_install.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><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></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 & 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#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#variant">variant</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#remark">remark</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#id2527183">Introduction</a></span></dt></dl></dd><dt><span class="chapter"><a href="sec_tactics.html">6. Tactics</a></span></dt><dd><dl><dt><span class="sect1"><a href="sec_tactics.html#tac_absurd">absurd</a></span></dt><dt><span class="sect1"><a href="tac_apply.html">apply</a></span></dt><dt><span class="sect1"><a href="tac_assumption.html">assumption</a></span></dt><dt><span class="sect1"><a href="tac_auto.html">auto</a></span></dt><dt><span class="sect1"><a href="tac_clear.html">clear</a></span></dt><dt><span class="sect1"><a href="tac_clearbody.html">clearbody</a></span></dt><dt><span class="sect1"><a href="tac_change.html">change</a></span></dt><dt><span class="sect1"><a href="tac_constructor.html">constructor</a></span></dt><dt><span class="sect1"><a href="tac_contradiction.html">contradiction</a></span></dt><dt><span class="sect1"><a href="tac_cut.html">cut</a></span></dt><dt><span class="sect1"><a href="tac_decompose.html">decompose</a></span></dt><dt><span class="sect1"><a href="tac_discriminate.html">discriminate</a></span></dt><dt><span class="sect1"><a href="tac_elim.html">elim</a></span></dt><dt><span class="sect1"><a href="tac_elimType.html">elimType</a></span></dt><dt><span class="sect1"><a href="tac_exact.html">exact</a></span></dt><dt><span class="sect1"><a href="tac_exists.html">exists</a></span></dt><dt><span class="sect1"><a href="tac_fail.html">failt</a></span></dt><dt><span class="sect1"><a href="tac_fold.html">fold</a></span></dt><dt><span class="sect1"><a href="tac_fourier.html">fourier</a></span></dt><dt><span class="sect1"><a href="tac_fwd.html">fwd</a></span></dt><dt><span class="sect1"><a href="tac_generalize.html">generalize</a></span></dt><dt><span class="sect1"><a href="tac_id.html">id</a></span></dt><dt><span class="sect1"><a href="tac_injection.html">injection</a></span></dt><dt><span class="sect1"><a href="tac_intro.html">intro</a></span></dt><dt><span class="sect1"><a href="tac_intros.html">intros</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_left.html">left</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_paramodulation.html">paramodulation</a></span></dt><dt><span class="sect1"><a href="tac_reduce.html">reduce</a></span></dt><dt><span class="sect1"><a href="tac_reflexivity.html">reflexivity</a></span></dt><dt><span class="sect1"><a href="tac_replace.html">change</a></span></dt><dt><span class="sect1"><a href="tac_rewrite.html">rewrite</a></span></dt><dt><span class="sect1"><a href="tac_right.html">right</a></span></dt><dt><span class="sect1"><a href="tac_ring.html">ring</a></span></dt><dt><span class="sect1"><a href="tac_simplify.html">simplify</a></span></dt><dt><span class="sect1"><a href="tac_split.html">split</a></span></dt><dt><span class="sect1"><a href="tac_symmetry.html">symmetry</a></span></dt><dt><span class="sect1"><a href="tac_transitivity.html">transitivity</a></span></dt><dt><span class="sect1"><a href="tac_unfold.html">unfold</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_tacticals.html">7. Tacticals</a></span></dt><dd><dl><dt><span class="sect1"><a href="sec_tacticals.html#id2535462">Introduction</a></span></dt></dl></dd><dt><span class="chapter"><a href="sec_commands.html">8. Other commands</a></span></dt><dd><dl><dt><span class="sect1"><a href="sec_commands.html#id2536001">Introduction</a></span></dt></dl></dd><dt><span class="chapter"><a href="sec_license.html">9. License</a></span></dt></dl></div><div class="list-of-figures"><p><b>List of Figures</b></p><dl><dt>3.1. <a href="authoring.html#id2521185">The Developments window</a></dt></dl></div><div class="list-of-tables"><p><b>List of Tables</b></p><dl><dt>2.1. <a href="sec_install.html#id2519563"> <span class="application">configure</span> command line
+ arguments</a></dt><dt>4.1. <a href="sec_terms.html#id2522091">id</a></dt><dt>4.2. <a href="sec_terms.html#id2522119">nat</a></dt><dt>4.3. <a href="sec_terms.html#id2522189">uri</a></dt><dt>4.4. <a href="sec_terms.html#id2522245">Terms</a></dt><dt>4.5. <a href="sec_terms.html#id2522798">Simple terms</a></dt><dt>4.6. <a href="sec_terms.html#id2523252">Arguments</a></dt><dt>4.7. <a href="sec_terms.html#id2523455">Miscellaneous arguments</a></dt><dt>4.8. <a href="sec_terms.html#id2523559">Pattern matching</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>
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>Proofs</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_terms.html" title="Chapter 4. Syntax" /><link rel="prev" href="axiom_definition_declaration.html" title="Definitions and declarations" /><link rel="next" href="sec_usernotation.html" title="Chapter 5. Extending the syntax" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">Proofs</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="axiom_definition_declaration.html">Prev</a> </td><th width="60%" align="center">Chapter 4. Syntax</th><td width="20%" align="right"> <a accesskey="n" href="sec_usernotation.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="proofs"></a>Proofs</h2></div></div></div><div class="sect2" lang="en" xml:lang="en"><div class="titlepage"><div><div><h3 class="title"><a id="theorem"></a><span class="bold"><strong>theorem</strong></span> <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>[<span class="bold"><strong>:</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>] [<span class="bold"><strong>≝</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>]</h3></div></div></div><p><strong class="userinput"><code>theorem f: P ≝ p</code></strong></p><p>Proves a new theorem <span><strong class="command">f</strong></span> whose thesis is
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>Proofs</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 User Manual (rev. 1α)" /><link rel="up" href="sec_terms.html" title="Chapter 4. Syntax" /><link rel="prev" href="axiom_definition_declaration.html" title="Definitions and declarations" /><link rel="next" href="sec_usernotation.html" title="Chapter 5. Extending the syntax" /></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">Proofs</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="axiom_definition_declaration.html">Prev</a> </td><th width="60%" align="center">Chapter 4. Syntax</th><td width="20%" align="right"> <a accesskey="n" href="sec_usernotation.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="proofs"></a>Proofs</h2></div></div></div><div class="sect2" lang="en" xml:lang="en"><div class="titlepage"><div><div><h3 class="title"><a id="theorem"></a><span class="bold"><strong>theorem</strong></span> <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>[<span class="bold"><strong>:</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>] [<span class="bold"><strong>≝</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>]</h3></div></div></div><p><strong class="userinput"><code>theorem f: P ≝ p</code></strong></p><p>Proves a new theorem <span><strong class="command">f</strong></span> whose thesis is
<span><strong class="command">P</strong></span>.</p><p>If <span><strong class="command">p</strong></span> is provided, it must be a proof term for
<span><strong class="command">P</strong></span>. Otherwise an interactive proof is started.</p><p><span><strong class="command">P</strong></span> can be omitted only if the proof is not
interactive.</p><p>Proving a theorem already proved in the library is an error.
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>Chapter 8. Other commands</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="prev" href="sec_tacticals.html" title="Chapter 7. Tacticals" /><link rel="next" href="sec_license.html" title="Chapter 9. License" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">Chapter 8. Other commands</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="sec_tacticals.html">Prev</a> </td><th width="60%" align="center"> </th><td width="20%" align="right"> <a accesskey="n" href="sec_license.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_commands"></a>Chapter 8. Other commands</h2></div></div></div><div class="toc"><p><b>Table of Contents</b></p><dl><dt><span class="sect1"><a href="sec_commands.html#id2535309">Introduction</a></span></dt></dl></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="id2535309"></a>Introduction</h2></div></div></div><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>Chapter 8. Other commands</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 User Manual (rev. 1α)" /><link rel="up" href="index.html" title="Matita V0.1.0 User Manual (rev. 1α)" /><link rel="prev" href="sec_tacticals.html" title="Chapter 7. Tacticals" /><link rel="next" href="sec_license.html" title="Chapter 9. License" /></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 8. Other commands</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="sec_tacticals.html">Prev</a> </td><th width="60%" align="center"> </th><td width="20%" align="right"> <a accesskey="n" href="sec_license.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_commands"></a>Chapter 8. Other commands</h2></div></div></div><div class="toc"><p><b>Table of Contents</b></p><dl><dt><span class="sect1"><a href="sec_commands.html#id2536001">Introduction</a></span></dt></dl></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="id2536001"></a>Introduction</h2></div></div></div><p>
<span class="emphasis"><em>TODO</em></span>
</p></div></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="sec_tacticals.html">Prev</a> </td><td width="20%" align="center"> </td><td width="40%" align="right"> <a accesskey="n" href="sec_license.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">Chapter 7. Tacticals </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> Chapter 9. License</td></tr></table></div></body></html>
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>Chapter 3. Getting started</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="prev" href="sec_install.html" title="Chapter 2. Installation" /><link rel="next" href="cicbrowser.html" title="Browsing and searching" /></head><body><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
+<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 User Manual (rev. 1α)" /><link rel="up" href="index.html" title="Matita V0.1.0 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
Constructions (CIC) and with interactive theorem provers with procedural
proof languages (expecially Coq), getting started with Matita is relatively
easy. You just need to learn how to type Unicode symbols, how to browse
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>Chapter 2. Installation</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="prev" href="WrtCoq.html" title="Matita vs Coq" /><link rel="next" href="sec_gettingstarted.html" title="Chapter 3. Getting started" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">Chapter 2. Installation</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="WrtCoq.html">Prev</a> </td><th width="60%" align="center"> </th><td width="20%" align="right"> <a accesskey="n" href="sec_gettingstarted.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_install"></a>Chapter 2. Installation</h2></div></div></div><div class="toc"><p><b>Table of Contents</b></p><dl><dt><span class="sect1"><a href="sec_install.html#inst_from_src">Installing from sources</a></span></dt><dd><dl><dt><span class="sect2"><a href="sec_install.html#get_source_code">Getting the source code</a></span></dt><dt><span class="sect2"><a href="sec_install.html#build_requirements">Requirements</a></span></dt><dt><span class="sect2"><a href="sec_install.html#database_setup">Database setup</a></span></dt><dt><span class="sect2"><a href="sec_install.html#build_instructions">Compiling and installing</a></span></dt></dl></dd></dl></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="inst_from_src"></a>Installing from sources</h2></div></div></div><p>Currently, the only intended way to install Matita is starting
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>Chapter 2. Installation</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 User Manual (rev. 1α)" /><link rel="up" href="index.html" title="Matita V0.1.0 User Manual (rev. 1α)" /><link rel="prev" href="WrtCoq.html" title="Matita vs Coq" /><link rel="next" href="sec_gettingstarted.html" title="Chapter 3. Getting started" /></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 2. Installation</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="WrtCoq.html">Prev</a> </td><th width="60%" align="center"> </th><td width="20%" align="right"> <a accesskey="n" href="sec_gettingstarted.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_install"></a>Chapter 2. Installation</h2></div></div></div><div class="toc"><p><b>Table of Contents</b></p><dl><dt><span class="sect1"><a href="sec_install.html#inst_from_src">Installing from sources</a></span></dt><dd><dl><dt><span class="sect2"><a href="sec_install.html#get_source_code">Getting the source code</a></span></dt><dt><span class="sect2"><a href="sec_install.html#build_requirements">Requirements</a></span></dt><dt><span class="sect2"><a href="sec_install.html#database_setup">Database setup</a></span></dt><dt><span class="sect2"><a href="sec_install.html#build_instructions">Compiling and installing</a></span></dt></dl></dd></dl></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="inst_from_src"></a>Installing from sources</h2></div></div></div><p>Currently, the only intended way to install Matita is starting
from its source code. </p><div class="sect2" lang="en" xml:lang="en"><div class="titlepage"><div><div><h3 class="title"><a id="get_source_code"></a>Getting the source code</h3></div></div></div><p>You can get the Matita source code in two ways:
</p><div class="orderedlist"><ol type="1"><li><p> go to the <a href="http://matita.cs.unibo.it/download.shtml" target="_top">download
page</a> and get the <a href="http://matita.cs.unibo.it/sources/matita-latest.tar.gz" target="_top">latest released source tarball</a>;</p></li><li><p> get the development sources from <a href="http://helm.cs.unibo.it/websvn/listing.php?repname=helm&path=%2F&sc=0" target="_top">our
parameters. They are listed in the table below, together with their
default values.
- </p><div class="table"><a id="id251
8871"></a><p class="title"><b>Table 2.1. <span class="application">configure</span> command line
+ </p><div class="table"><a id="id251
9563"></a><p class="title"><b>Table 2.1. <span class="application">configure</span> command line
arguments</b></p><table summary=" configure command line 	 arguments" border="1"><colgroup><col /><col /><col /></colgroup><thead><tr><th align="center">Argument</th><th align="center">Default</th><th align="center">Description</th></tr></thead><tbody><tr><td align="left">
<strong class="userinput"><code>--with-runtime-dir=<em class="replaceable"><code>dir</code></em></code></strong>
</td><td align="left"> <code class="filename">/usr/local/matita/</code> </td><td align="left"> <p> Runtime base directory where all Matita stuff
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>Chapter 1. Introduction</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="prev" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="next" href="WrtCoq.html" title="Matita vs Coq" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">Chapter 1. Introduction</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="index.html">Prev</a> </td><th width="60%" align="center"> </th><td width="20%" align="right"> <a accesskey="n" href="WrtCoq.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_intro"></a>Chapter 1. Introduction</h2></div></div></div><div class="toc"><p><b>Table of Contents</b></p><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></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="Features"></a>Features</h2></div></div></div><p><span class="application">Matita</span> is an interactive theorem prover
- (or proof assistant) with the following characteristics:</p><div class="itemizedlist"><ul type="disc"><li><p>It is based on a variant of the Calculus of (
co)Inductive Constructions (CIC). CIC is also the logic of the Coq proof assistant.</p></li><li><p>It adopts a procedural proof language, but it has a new set of small step tacticals that improve proof structuring and debugging.</p></li><li><p>It has a stand-alone graphical user interface (GUI) inspired by
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>Chapter 1. Introduction</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 User Manual (rev. 1α)" /><link rel="up" href="index.html" title="Matita V0.1.0 User Manual (rev. 1α)" /><link rel="prev" href="index.html" title="Matita V0.1.0 User Manual (rev. 1α)" /><link rel="next" href="WrtCoq.html" title="Matita vs Coq" /></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 1. Introduction</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="index.html">Prev</a> </td><th width="60%" align="center"> </th><td width="20%" align="right"> <a accesskey="n" href="WrtCoq.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_intro"></a>Chapter 1. Introduction</h2></div></div></div><div class="toc"><p><b>Table of Contents</b></p><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></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="Features"></a>Features</h2></div></div></div><p><span class="application">Matita</span> is an interactive theorem prover
+ (or proof assistant) with the following characteristics:</p><div class="itemizedlist"><ul type="disc"><li><p>It is based on a variant of the Calculus of (
Co)Inductive Constructions (CIC). CIC is also the logic of the Coq proof assistant.</p></li><li><p>It adopts a procedural proof language, but it has a new set of small step tacticals that improve proof structuring and debugging.</p></li><li><p>It has a stand-alone graphical user interface (GUI) inspired by
CtCoq/Proof General. The GUI is implemented according to the state
of the art. In particular:</p><div class="itemizedlist"><ul type="circle"><li><p>It is based and fully integrated with Gtk/Gnome.</p></li><li><p>An on-line help can be browsed via the Gnome documentation browser.</p></li><li><p>Mathematical formulae are rendered in two dimensional notation via MathML and Unicode.</p></li></ul></div></li><li><p>It integrates advanced browsing and searching procedures.</p></li><li><p>It allows the use of the typical ambiguous mathematical notation by means of a disambiguating parser.</p></li><li><p>It is compatible with the library of Coq (definitions and proof objects).</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="index.html">Prev</a> </td><td width="20%" align="center"> </td><td width="40%" align="right"> <a accesskey="n" href="WrtCoq.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top"><span class="application">Matita</span> V0.1.0
-
Manual (rev. 0) </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> Matita vs Coq</td></tr></table></div></body></html>
+
User Manual (rev. 1α) </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> Matita vs Coq</td></tr></table></div></body></html>
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>Chapter 9. License</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="prev" href="sec_commands.html" title="Chapter 8. Other commands" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">Chapter 9. License</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="sec_commands.html">Prev</a> </td><th width="60%" align="center"> </th><td width="20%" align="right"> </td></tr></table><hr /></div><div class="chapter" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title"><a id="sec_license"></a>Chapter 9. License</h2></div></div></div><p> This file is part of HELM, an Hypertextual, Electronic Library of
- Mathematics, developed at the Computer Science Department, University of
-
Bologna, Italy. </p><p> HELM is free software; you can redistribute it and/or modify it under
- the terms of the GNU General Public License as published by the Free
- Software Foundation; either version 2 of the License, or (at your option)
- any later version. </p><p> HELM is distributed in the hope that it will be useful, but WITHOUT
- ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
- FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for
- more details. </p><p> You should have received a copy of the GNU General Public License
- along with HELM; if not, write to the Free Software Foundation, Inc., 59
- Temple Place - Suite 330, Boston, MA 02111-1307, USA. A copy of the GNU
-
General Public License is available at <a href="ghelp:gpl" target="_top">this link</a>. </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="sec_commands.html">Prev</a> </td><td width="20%" align="center"> </td><td width="40%" align="right"> </td></tr><tr><td width="40%" align="left" valign="top">Chapter 8. Other commands </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> </td></tr></table></div></body></html>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>Chapter 9. License</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 User Manual (rev. 1α)" /><link rel="up" href="index.html" title="Matita V0.1.0 User Manual (rev. 1α)" /><link rel="prev" href="sec_commands.html" title="Chapter 8. Other commands" /></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 9. License</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="sec_commands.html">Prev</a> </td><th width="60%" align="center"> </th><td width="20%" align="right"> </td></tr></table><hr /></div><div class="chapter" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title"><a id="sec_license"></a>Chapter 9. License</h2></div></div></div><p> Both Matita and this document are part of HELM, an Hypertextual,
+ Electronic Library of Mathematics, developed at the Computer Science
+
Department, University of Bologna, Italy. </p><p> HELM is free software; you can redistribute it and/or modify it under
+ the terms of the GNU General Public License as published by the Free Software
+ Foundation; either version 2 of the License, or (at your option) any later
+ version. </p><p> HELM is distributed in the hope that it will be useful, but WITHOUT ANY
+ WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR
+ A PARTICULAR PURPOSE. See the GNU General Public License for more details.
+</p><p> You should have received a copy of the GNU General Public License along
+ with HELM; if not, write to the Free Software Foundation, Inc., 51 Franklin
+ St, Fifth Floor, Boston, MA 02110-1301 USA. A copy of the GNU General
+
Public License is available at <a href="http://www.gnu.org/copyleft/gpl.html" target="_top">this link</a>. </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="sec_commands.html">Prev</a> </td><td width="20%" align="center"> </td><td width="40%" align="right"> </td></tr><tr><td width="40%" align="left" valign="top">Chapter 8. Other commands </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> </td></tr></table></div></body></html>
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>Chapter 7. Tacticals</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="prev" href="tac_whd.html" title="whd <pattern>" /><link rel="next" href="sec_commands.html" title="Chapter 8. Other commands" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">Chapter 7. Tacticals</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_whd.html">Prev</a> </td><th width="60%" align="center"> </th><td width="20%" align="right"> <a accesskey="n" href="sec_commands.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_tacticals"></a>Chapter 7. Tacticals</h2></div></div></div><div class="toc"><p><b>Table of Contents</b></p><dl><dt><span class="sect1"><a href="sec_tacticals.html#id2534769">Introduction</a></span></dt></dl></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="id2534769"></a>Introduction</h2></div></div></div><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>Chapter 7. Tacticals</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 User Manual (rev. 1α)" /><link rel="up" href="index.html" title="Matita V0.1.0 User Manual (rev. 1α)" /><link rel="prev" href="tac_whd.html" title="whd <pattern>" /><link rel="next" href="sec_commands.html" title="Chapter 8. Other commands" /></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 7. Tacticals</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_whd.html">Prev</a> </td><th width="60%" align="center"> </th><td width="20%" align="right"> <a accesskey="n" href="sec_commands.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_tacticals"></a>Chapter 7. Tacticals</h2></div></div></div><div class="toc"><p><b>Table of Contents</b></p><dl><dt><span class="sect1"><a href="sec_tacticals.html#id2535462">Introduction</a></span></dt></dl></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="id2535462"></a>Introduction</h2></div></div></div><p>
<span class="emphasis"><em>TODO</em></span>
</p></div></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_whd.html">Prev</a> </td><td width="20%" align="center"> </td><td width="40%" align="right"> <a accesskey="n" href="sec_commands.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">whd <pattern> </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> Chapter 8. Other commands</td></tr></table></div></body></html>
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>Chapter 6. Tactics</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="prev" href="sec_usernotation.html" title="Chapter 5. Extending the syntax" /><link rel="next" href="tac_apply.html" title="apply sterm" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">Chapter 6. Tactics</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="sec_usernotation.html">Prev</a> </td><th width="60%" align="center"> </th><td width="20%" align="right"> <a accesskey="n" href="tac_apply.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_tactics"></a>Chapter 6. Tactics</h2></div></div></div><div class="toc"><p><b>Table of Contents</b></p><dl><dt><span class="sect1"><a href="sec_tactics.html#tac_absurd">absurd</a></span></dt><dt><span class="sect1"><a href="tac_apply.html">apply</a></span></dt><dt><span class="sect1"><a href="tac_assumption.html">assumption</a></span></dt><dt><span class="sect1"><a href="tac_auto.html">auto</a></span></dt><dt><span class="sect1"><a href="tac_clear.html">clear</a></span></dt><dt><span class="sect1"><a href="tac_clearbody.html">clearbody</a></span></dt><dt><span class="sect1"><a href="tac_change.html">change</a></span></dt><dt><span class="sect1"><a href="tac_constructor.html">constructor</a></span></dt><dt><span class="sect1"><a href="tac_contradiction.html">contradiction</a></span></dt><dt><span class="sect1"><a href="tac_cut.html">cut</a></span></dt><dt><span class="sect1"><a href="tac_decompose.html">decompose</a></span></dt><dt><span class="sect1"><a href="tac_discriminate.html">discriminate</a></span></dt><dt><span class="sect1"><a href="tac_elim.html">elim</a></span></dt><dt><span class="sect1"><a href="tac_elimType.html">elimType</a></span></dt><dt><span class="sect1"><a href="tac_exact.html">exact</a></span></dt><dt><span class="sect1"><a href="tac_exists.html">exists</a></span></dt><dt><span class="sect1"><a href="tac_fail.html">failt</a></span></dt><dt><span class="sect1"><a href="tac_fold.html">fold</a></span></dt><dt><span class="sect1"><a href="tac_fourier.html">fourier</a></span></dt><dt><span class="sect1"><a href="tac_fwd.html">fwd</a></span></dt><dt><span class="sect1"><a href="tac_generalize.html">generalize</a></span></dt><dt><span class="sect1"><a href="tac_id.html">id</a></span></dt><dt><span class="sect1"><a href="tac_injection.html">injection</a></span></dt><dt><span class="sect1"><a href="tac_intro.html">intro</a></span></dt><dt><span class="sect1"><a href="tac_intros.html">intros</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_left.html">left</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_paramodulation.html">paramodulation</a></span></dt><dt><span class="sect1"><a href="tac_reduce.html">reduce</a></span></dt><dt><span class="sect1"><a href="tac_reflexivity.html">reflexivity</a></span></dt><dt><span class="sect1"><a href="tac_replace.html">change</a></span></dt><dt><span class="sect1"><a href="tac_rewrite.html">rewrite</a></span></dt><dt><span class="sect1"><a href="tac_right.html">right</a></span></dt><dt><span class="sect1"><a href="tac_ring.html">ring</a></span></dt><dt><span class="sect1"><a href="tac_simplify.html">simplify</a></span></dt><dt><span class="sect1"><a href="tac_split.html">split</a></span></dt><dt><span class="sect1"><a href="tac_symmetry.html">symmetry</a></span></dt><dt><span class="sect1"><a href="tac_transitivity.html">transitivity</a></span></dt><dt><span class="sect1"><a href="tac_unfold.html">unfold</a></span></dt><dt><span class="sect1"><a href="tac_whd.html">whd</a></span></dt></dl></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_absurd"></a>absurd <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span></h2></div></div></div><p><strong class="userinput"><code>absurd P</code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>Chapter 6. Tactics</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 User Manual (rev. 1α)" /><link rel="up" href="index.html" title="Matita V0.1.0 User Manual (rev. 1α)" /><link rel="prev" href="sec_usernotation.html" title="Chapter 5. Extending the syntax" /><link rel="next" href="tac_apply.html" title="apply sterm" /></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 6. Tactics</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="sec_usernotation.html">Prev</a> </td><th width="60%" align="center"> </th><td width="20%" align="right"> <a accesskey="n" href="tac_apply.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_tactics"></a>Chapter 6. Tactics</h2></div></div></div><div class="toc"><p><b>Table of Contents</b></p><dl><dt><span class="sect1"><a href="sec_tactics.html#tac_absurd">absurd</a></span></dt><dt><span class="sect1"><a href="tac_apply.html">apply</a></span></dt><dt><span class="sect1"><a href="tac_assumption.html">assumption</a></span></dt><dt><span class="sect1"><a href="tac_auto.html">auto</a></span></dt><dt><span class="sect1"><a href="tac_clear.html">clear</a></span></dt><dt><span class="sect1"><a href="tac_clearbody.html">clearbody</a></span></dt><dt><span class="sect1"><a href="tac_change.html">change</a></span></dt><dt><span class="sect1"><a href="tac_constructor.html">constructor</a></span></dt><dt><span class="sect1"><a href="tac_contradiction.html">contradiction</a></span></dt><dt><span class="sect1"><a href="tac_cut.html">cut</a></span></dt><dt><span class="sect1"><a href="tac_decompose.html">decompose</a></span></dt><dt><span class="sect1"><a href="tac_discriminate.html">discriminate</a></span></dt><dt><span class="sect1"><a href="tac_elim.html">elim</a></span></dt><dt><span class="sect1"><a href="tac_elimType.html">elimType</a></span></dt><dt><span class="sect1"><a href="tac_exact.html">exact</a></span></dt><dt><span class="sect1"><a href="tac_exists.html">exists</a></span></dt><dt><span class="sect1"><a href="tac_fail.html">failt</a></span></dt><dt><span class="sect1"><a href="tac_fold.html">fold</a></span></dt><dt><span class="sect1"><a href="tac_fourier.html">fourier</a></span></dt><dt><span class="sect1"><a href="tac_fwd.html">fwd</a></span></dt><dt><span class="sect1"><a href="tac_generalize.html">generalize</a></span></dt><dt><span class="sect1"><a href="tac_id.html">id</a></span></dt><dt><span class="sect1"><a href="tac_injection.html">injection</a></span></dt><dt><span class="sect1"><a href="tac_intro.html">intro</a></span></dt><dt><span class="sect1"><a href="tac_intros.html">intros</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_left.html">left</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_paramodulation.html">paramodulation</a></span></dt><dt><span class="sect1"><a href="tac_reduce.html">reduce</a></span></dt><dt><span class="sect1"><a href="tac_reflexivity.html">reflexivity</a></span></dt><dt><span class="sect1"><a href="tac_replace.html">change</a></span></dt><dt><span class="sect1"><a href="tac_rewrite.html">rewrite</a></span></dt><dt><span class="sect1"><a href="tac_right.html">right</a></span></dt><dt><span class="sect1"><a href="tac_ring.html">ring</a></span></dt><dt><span class="sect1"><a href="tac_simplify.html">simplify</a></span></dt><dt><span class="sect1"><a href="tac_split.html">split</a></span></dt><dt><span class="sect1"><a href="tac_symmetry.html">symmetry</a></span></dt><dt><span class="sect1"><a href="tac_transitivity.html">transitivity</a></span></dt><dt><span class="sect1"><a href="tac_unfold.html">unfold</a></span></dt><dt><span class="sect1"><a href="tac_whd.html">whd</a></span></dt></dl></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_absurd"></a>absurd <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span></h2></div></div></div><p><strong class="userinput"><code>absurd P</code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p><span><strong class="command">P</strong></span> must have type <span><strong class="command">Prop</strong></span>.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It closes the current sequent by eliminating an
absurd term.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>It opens two new sequents of conclusion <span><strong class="command">P</strong></span>
and <span><strong class="command">¬P</strong></span>.</p></dd></dl></div><p>
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>Chapter 4. Syntax</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="prev" href="authoring.html" title="Authoring" /><link rel="next" href="axiom_definition_declaration.html" title="Definitions and declarations" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">Chapter 4. Syntax</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="authoring.html">Prev</a> </td><th width="60%" align="center"> </th><td width="20%" align="right"> <a accesskey="n" href="axiom_definition_declaration.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_terms"></a>Chapter 4. Syntax</h2></div></div></div><div class="toc"><p><b>Table of Contents</b></p><dl><dt><span class="sect1"><a href="sec_terms.html#terms_and_co">Terms & 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#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#variant">variant</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#remark">remark</a></span></dt></dl></dd></dl></div><p>To describe syntax in this manual we use the following conventions:</p><div class="orderedlist"><ol type="1"><li><p>Non terminal symbols are emphasized and have a link to their
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>Chapter 4. Syntax</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 User Manual (rev. 1α)" /><link rel="up" href="index.html" title="Matita V0.1.0 User Manual (rev. 1α)" /><link rel="prev" href="authoring.html" title="Authoring" /><link rel="next" href="axiom_definition_declaration.html" title="Definitions and declarations" /></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 4. Syntax</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="authoring.html">Prev</a> </td><th width="60%" align="center"> </th><td width="20%" align="right"> <a accesskey="n" href="axiom_definition_declaration.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_terms"></a>Chapter 4. Syntax</h2></div></div></div><div class="toc"><p><b>Table of Contents</b></p><dl><dt><span class="sect1"><a href="sec_terms.html#terms_and_co">Terms & 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#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#variant">variant</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#remark">remark</a></span></dt></dl></dd></dl></div><p>To describe syntax in this manual we use the following conventions:</p><div class="orderedlist"><ol type="1"><li><p>Non terminal symbols are emphasized and have a link to their
definition. E.g.: <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span></p></li><li><p>Terminal symbols are in bold. E.g.:
<span class="bold"><strong>theorem</strong></span></p></li><li><p>Optional sequences of elements are put in square brackets.
E.g.: [<span class="bold"><strong>in</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>]</p></li><li><p>Alternatives are put in square brakets and they are
separated by vertical bars. E.g.: [<span class="bold"><strong><</strong></span>|<span class="bold"><strong>></strong></span>]</p></li><li><p>Repetition of sequences of elements are given by putting the
first sequence in square brackets, that are followed by three dots.
E.g.: [<span class="bold"><strong>and</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>]…</p></li></ol></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="terms_and_co"></a>Terms & co.</h2></div></div></div><div class="sect2" lang="en" xml:lang="en"><div class="titlepage"><div><div><h3 class="title"><a id="lexical"></a>Lexical conventions</h3></div></div></div><p>
- </p><div class="table"><a id="id252
1399"></a><p class="title"><b>Table 4.1. id</b></p><table summary="id" border="1"><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td><a id="id"></a><span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span></td><td>::=</td><td><span class="emphasis"><em>〈〈<span class="emphasis"><em>TODO</em></span>〉〉</em></span></td><td class="auto-generated"> </td></tr></tbody></table></div><p>
- </p><div class="table"><a id="id252
1488"></a><p class="title"><b>Table 4.2. nat</b></p><table summary="nat" border="1"><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td><a id="nat"></a><span class="emphasis"><em><a href="sec_terms.html#nat">nat</a></em></span></td><td>::=</td><td><span class="emphasis"><em>〈〈<span class="emphasis"><em>TODO</em></span>〉〉</em></span></td><td class="auto-generated"> </td></tr></tbody></table></div><p>
- </p><div class="table"><a id="id252
1498"></a><p class="title"><b>Table 4.3. uri</b></p><table summary="uri" border="1"><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td><a id="uri"></a><span class="emphasis"><em><a href="sec_terms.html#uri">uri</a></em></span></td><td>::=</td><td><span class="emphasis"><em>〈〈<span class="emphasis"><em>TODO</em></span>〉〉</em></span></td><td class="auto-generated"> </td></tr></tbody></table></div><p>
+ </p><div class="table"><a id="id252
2091"></a><p class="title"><b>Table 4.1. id</b></p><table summary="id" border="1"><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td><a id="id"></a><span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span></td><td>::=</td><td><span class="emphasis"><em>〈〈<span class="emphasis"><em>TODO</em></span>〉〉</em></span></td><td class="auto-generated"> </td></tr></tbody></table></div><p>
+ </p><div class="table"><a id="id252
2119"></a><p class="title"><b>Table 4.2. nat</b></p><table summary="nat" border="1"><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td><a id="nat"></a><span class="emphasis"><em><a href="sec_terms.html#nat">nat</a></em></span></td><td>::=</td><td><span class="emphasis"><em>〈〈<span class="emphasis"><em>TODO</em></span>〉〉</em></span></td><td class="auto-generated"> </td></tr></tbody></table></div><p>
+ </p><div class="table"><a id="id252
2189"></a><p class="title"><b>Table 4.3. uri</b></p><table summary="uri" border="1"><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td><a id="uri"></a><span class="emphasis"><em><a href="sec_terms.html#uri">uri</a></em></span></td><td>::=</td><td><span class="emphasis"><em>〈〈<span class="emphasis"><em>TODO</em></span>〉〉</em></span></td><td class="auto-generated"> </td></tr></tbody></table></div><p>
</p></div><div class="sect2" lang="en" xml:lang="en"><div class="titlepage"><div><div><h3 class="title"><a id="terms"></a>Terms</h3></div></div></div><p>
- </p><div class="table"><a id="id252
1554"></a><p class="title"><b>Table 4.4. Terms</b></p><table summary="Terms" border="1"><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td><a id="term"></a><span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span></td><td>::=</td><td><span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span></td><td>simple or delimited term</td></tr><tr><td> </td><td>|</td><td><span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span></td><td>application</td></tr><tr><td> </td><td>|</td><td><span class="bold"><strong>λ</strong></span><span class="emphasis"><em><a href="sec_terms.html#args">args</a></em></span><span class="bold"><strong>.</strong></span><span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span></td><td>λ-abstraction</td></tr><tr><td> </td><td>|</td><td><span class="bold"><strong>Π</strong></span><span class="emphasis"><em><a href="sec_terms.html#args">args</a></em></span><span class="bold"><strong>.</strong></span><span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span></td><td>dependent product meant to define a datatype</td></tr><tr><td> </td><td>|</td><td><span class="bold"><strong>∀</strong></span><span class="emphasis"><em><a href="sec_terms.html#args">args</a></em></span><span class="bold"><strong>.</strong></span><span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span></td><td>dependent product meant to define a proposition</td></tr><tr><td> </td><td>|</td><td><span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span> <span class="bold"><strong>→</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span></td><td>non-dependent product (logical implication or function space)</td></tr><tr><td> </td><td>|</td><td><span class="bold"><strong>let</strong></span> [<span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>|(<span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span><span class="bold"><strong>:</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>)] <span class="bold"><strong>≝</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span> <span class="bold"><strong>in</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span></td><td>local definition</td></tr><tr><td> </td><td>|</td><td><span class="bold"><strong>let</strong></span>
+ </p><div class="table"><a id="id252
2245"></a><p class="title"><b>Table 4.4. Terms</b></p><table summary="Terms" border="1"><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td><a id="term"></a><span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span></td><td>::=</td><td><span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span></td><td>simple or delimited term</td></tr><tr><td> </td><td>|</td><td><span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span></td><td>application</td></tr><tr><td> </td><td>|</td><td><span class="bold"><strong>λ</strong></span><span class="emphasis"><em><a href="sec_terms.html#args">args</a></em></span><span class="bold"><strong>.</strong></span><span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span></td><td>λ-abstraction</td></tr><tr><td> </td><td>|</td><td><span class="bold"><strong>Π</strong></span><span class="emphasis"><em><a href="sec_terms.html#args">args</a></em></span><span class="bold"><strong>.</strong></span><span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span></td><td>dependent product meant to define a datatype</td></tr><tr><td> </td><td>|</td><td><span class="bold"><strong>∀</strong></span><span class="emphasis"><em><a href="sec_terms.html#args">args</a></em></span><span class="bold"><strong>.</strong></span><span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span></td><td>dependent product meant to define a proposition</td></tr><tr><td> </td><td>|</td><td><span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span> <span class="bold"><strong>→</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span></td><td>non-dependent product (logical implication or function space)</td></tr><tr><td> </td><td>|</td><td><span class="bold"><strong>let</strong></span> [<span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>|(<span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span><span class="bold"><strong>:</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>)] <span class="bold"><strong>≝</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span> <span class="bold"><strong>in</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span></td><td>local definition</td></tr><tr><td> </td><td>|</td><td><span class="bold"><strong>let</strong></span>
[<span class="bold"><strong>co</strong></span>]<span class="bold"><strong>rec</strong></span>
<span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span> [<span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>|<span class="bold"><strong>(</strong></span><span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>[<span class="bold"><strong>,</strong></span><span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>]… <span class="bold"><strong>:</strong></span><span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span><span class="bold"><strong>)</strong></span>]… [<span class="bold"><strong>on</strong></span> <span class="emphasis"><em><a href="sec_terms.html#nat">nat</a></em></span>]
[<span class="bold"><strong>:</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>]
<span class="bold"><strong>in</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>
</td><td> </td></tr><tr><td> </td><td>|</td><td>…</td><td>user provided notation</td></tr></tbody></table></div><p>
- </p><div class="table"><a id="id2522
106"></a><p class="title"><b>Table 4.5. Simple terms</b></p><table summary="Simple terms" border="1"><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td><a id="sterm"></a><span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span></td><td>::=</td><td><span class="bold"><strong>(</strong></span><span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span><span class="bold"><strong>)</strong></span></td><td> </td></tr><tr><td> </td><td>|</td><td><span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>[<span class="bold"><strong>\subst[</strong></span>
+ </p><div class="table"><a id="id2522
798"></a><p class="title"><b>Table 4.5. Simple terms</b></p><table summary="Simple terms" border="1"><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td><a id="sterm"></a><span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span></td><td>::=</td><td><span class="bold"><strong>(</strong></span><span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span><span class="bold"><strong>)</strong></span></td><td> </td></tr><tr><td> </td><td>|</td><td><span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>[<span class="bold"><strong>\subst[</strong></span>
<span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span><span class="bold"><strong>≔</strong></span><span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>
[<span class="bold"><strong>;</strong></span><span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span><span class="bold"><strong>≔</strong></span><span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>]…
<span class="bold"><strong>]</strong></span>]
<span class="emphasis"><em><a href="sec_terms.html#match_pattern">match_pattern</a></em></span> <span class="bold"><strong> ⇒ </strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>
]…<span class="bold"><strong>]</strong></span> </td><td> </td></tr><tr><td> </td><td>|</td><td><span class="bold"><strong>(</strong></span><span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span><span class="bold"><strong>:</strong></span><span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span><span class="bold"><strong>)</strong></span></td><td>cast</td></tr><tr><td> </td><td>|</td><td>…</td><td>user provided notation at precedence 90</td></tr></tbody></table></div><p>
- </p><div class="table"><a id="id252
2561"></a><p class="title"><b>Table 4.6. Arguments</b></p><table summary="Arguments" border="1"><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td><a id="args"></a><span class="emphasis"><em><a href="sec_terms.html#args">args</a></em></span></td><td>::=</td><td>
+ </p><div class="table"><a id="id252
3252"></a><p class="title"><b>Table 4.6. Arguments</b></p><table summary="Arguments" border="1"><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td><a id="args"></a><span class="emphasis"><em><a href="sec_terms.html#args">args</a></em></span></td><td>::=</td><td>
<span class="bold"><strong>_</strong></span>[<span class="bold"><strong>:</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>]
</td><td>ignored argument</td></tr><tr><td> </td><td>|</td><td>
<span class="bold"><strong>(</strong></span><span class="bold"><strong>_</strong></span>[<span class="bold"><strong>:</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>]<span class="bold"><strong>)</strong></span>
</td><td>ignored argument</td></tr><tr><td> </td><td>|</td><td><span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>[<span class="bold"><strong>,</strong></span><span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>]…[<span class="bold"><strong>:</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>]</td><td> </td></tr><tr><td> </td><td>|</td><td><span class="bold"><strong>(</strong></span><span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>[<span class="bold"><strong>,</strong></span><span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>]…[<span class="bold"><strong>:</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span>]<span class="bold"><strong>)</strong></span></td><td> </td></tr></tbody></table></div><p>
- </p><div class="table"><a id="id252
2763"></a><p class="title"><b>Table 4.7. Miscellaneous arguments</b></p><table summary="Miscellaneous arguments" border="1"><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td><a id="args2"></a><span class="emphasis"><em><a href="sec_terms.html#args2">args2</a></em></span></td><td>::=</td><td><span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span></td><td> </td></tr><tr><td> </td><td>|</td><td><span class="bold"><strong>(</strong></span><span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>[<span class="bold"><strong>,</strong></span><span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>]…<span class="bold"><strong>:</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span><span class="bold"><strong>)</strong></span></td><td> </td></tr></tbody></table></div><p>
+ </p><div class="table"><a id="id252
3455"></a><p class="title"><b>Table 4.7. Miscellaneous arguments</b></p><table summary="Miscellaneous arguments" border="1"><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td><a id="args2"></a><span class="emphasis"><em><a href="sec_terms.html#args2">args2</a></em></span></td><td>::=</td><td><span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span></td><td> </td></tr><tr><td> </td><td>|</td><td><span class="bold"><strong>(</strong></span><span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>[<span class="bold"><strong>,</strong></span><span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>]…<span class="bold"><strong>:</strong></span> <span class="emphasis"><em><a href="sec_terms.html#term">term</a></em></span><span class="bold"><strong>)</strong></span></td><td> </td></tr></tbody></table></div><p>
- </p><div class="table"><a id="id252
2867"></a><p class="title"><b>Table 4.8. Pattern matching</b></p><table summary="Pattern matching" border="1"><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td><a id="match_pattern"></a><span class="emphasis"><em><a href="sec_terms.html#match_pattern">match_pattern</a></em></span></td><td>::=</td><td><span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span></td><td>0-ary constructor</td></tr><tr><td> </td><td>|</td><td><span class="bold"><strong>(</strong></span><span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span> <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span> [<span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>]…<span class="bold"><strong>)</strong></span></td><td>n-ary constructor (binds the n arguments)</td></tr></tbody></table></div><p>
+ </p><div class="table"><a id="id252
3559"></a><p class="title"><b>Table 4.8. Pattern matching</b></p><table summary="Pattern matching" border="1"><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td><a id="match_pattern"></a><span class="emphasis"><em><a href="sec_terms.html#match_pattern">match_pattern</a></em></span></td><td>::=</td><td><span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span></td><td>0-ary constructor</td></tr><tr><td> </td><td>|</td><td><span class="bold"><strong>(</strong></span><span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span> <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span> [<span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>]…<span class="bold"><strong>)</strong></span></td><td>n-ary constructor (binds the n arguments)</td></tr></tbody></table></div><p>
</p></div></div></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="authoring.html">Prev</a> </td><td width="20%" align="center"> </td><td width="40%" align="right"> <a accesskey="n" href="axiom_definition_declaration.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">Authoring </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> Definitions and declarations</td></tr></table></div></body></html>
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>Chapter 5. Extending the syntax</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="prev" href="proofs.html" title="Proofs" /><link rel="next" href="sec_tactics.html" title="Chapter 6. Tactics" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">Chapter 5. Extending the syntax</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="proofs.html">Prev</a> </td><th width="60%" align="center"> </th><td width="20%" align="right"> <a accesskey="n" href="sec_tactics.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_usernotation"></a>Chapter 5. Extending the syntax</h2></div></div></div><div class="toc"><p><b>Table of Contents</b></p><dl><dt><span class="sect1"><a href="sec_usernotation.html#id2526491">Introduction</a></span></dt></dl></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="id2526491"></a>Introduction</h2></div></div></div><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>Chapter 5. Extending the syntax</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 User Manual (rev. 1α)" /><link rel="up" href="index.html" title="Matita V0.1.0 User Manual (rev. 1α)" /><link rel="prev" href="proofs.html" title="Proofs" /><link rel="next" href="sec_tactics.html" title="Chapter 6. Tactics" /></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 5. Extending the syntax</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="proofs.html">Prev</a> </td><th width="60%" align="center"> </th><td width="20%" align="right"> <a accesskey="n" href="sec_tactics.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_usernotation"></a>Chapter 5. Extending the syntax</h2></div></div></div><div class="toc"><p><b>Table of Contents</b></p><dl><dt><span class="sect1"><a href="sec_usernotation.html#id2527183">Introduction</a></span></dt></dl></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="id2527183"></a>Introduction</h2></div></div></div><p>
<span class="emphasis"><em>TODO</em></span>
</p></div></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="proofs.html">Prev</a> </td><td width="20%" align="center"> </td><td width="40%" align="right"> <a accesskey="n" href="sec_tactics.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">Proofs </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> Chapter 6. Tactics</td></tr></table></div></body></html>
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>apply sterm</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="next" href="tac_assumption.html" title="assumption" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">apply sterm</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="sec_tactics.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_assumption.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="tac_apply"></a>apply <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span></h2></div></div></div><p><strong class="userinput"><code>apply t</code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>apply sterm</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 User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="next" href="tac_assumption.html" title="assumption" /></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">apply sterm</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="sec_tactics.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_assumption.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="tac_apply"></a>apply <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span></h2></div></div></div><p><strong class="userinput"><code>apply t</code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p><span><strong class="command">t</strong></span> must have type
<span><strong class="command">T<sub>1</sub> → ... →
T<sub>n</sub> → G</strong></span>
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>assumption</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_apply.html" title="apply sterm" /><link rel="next" href="tac_auto.html" title="auto [depth=nat] [width=nat] [paramodulation] [full]" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">assumption</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_apply.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_auto.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="tac_assumption"></a>assumption</h2></div></div></div><p><strong class="userinput"><code>assumption </code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>assumption</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 User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_apply.html" title="apply sterm" /><link rel="next" href="tac_auto.html" title="auto [depth=nat] [width=nat] [paramodulation] [full]" /></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">assumption</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_apply.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_auto.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="tac_assumption"></a>assumption</h2></div></div></div><p><strong class="userinput"><code>assumption </code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>There must exist an hypothesis whose type can be unified with
the conclusion of the current sequent.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It closes the current sequent exploiting an hypothesis.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>None</p></dd></dl></div><p>
</p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_apply.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_auto.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">apply sterm </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> auto [depth=nat] [width=nat] [paramodulation] [full]</td></tr></table></div></body></html>
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>auto [depth=nat] [width=nat] [paramodulation] [full]</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_assumption.html" title="assumption" /><link rel="next" href="tac_clear.html" title="clear id" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">auto [depth=nat] [width=nat] [paramodulation] [full]</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_assumption.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_clear.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="tac_auto"></a>auto [depth=<span class="emphasis"><em><a href="sec_terms.html#nat">nat</a></em></span>] [width=<span class="emphasis"><em><a href="sec_terms.html#nat">nat</a></em></span>] [paramodulation] [full]</h2></div></div></div><p><strong class="userinput"><code>auto depth=d width=w paramodulation full</code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>auto [depth=nat] [width=nat] [paramodulation] [full]</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 User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_assumption.html" title="assumption" /><link rel="next" href="tac_clear.html" title="clear id" /></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">auto [depth=nat] [width=nat] [paramodulation] [full]</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_assumption.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_clear.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="tac_auto"></a>auto [depth=<span class="emphasis"><em><a href="sec_terms.html#nat">nat</a></em></span>] [width=<span class="emphasis"><em><a href="sec_terms.html#nat">nat</a></em></span>] [paramodulation] [full]</h2></div></div></div><p><strong class="userinput"><code>auto depth=d width=w paramodulation full</code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>None, but the tactic may fail finding a proof if every
proof is in the search space that is pruned away. Pruning is
controlled by <span><strong class="command">d</strong></span> and <span><strong class="command">w</strong></span>.
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>change <pattern> with sterm</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_clearbody.html" title="clearbody id" /><link rel="next" href="tac_constructor.html" title="constructor nat" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">change <pattern> with sterm</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_clearbody.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_constructor.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="tac_change"></a>change <pattern> with <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span></h2></div></div></div><p><strong class="userinput"><code>change patt with t</code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>change <pattern> with sterm</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 User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_clearbody.html" title="clearbody id" /><link rel="next" href="tac_constructor.html" title="constructor nat" /></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">change <pattern> with sterm</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_clearbody.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_constructor.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="tac_change"></a>change <pattern> with <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span></h2></div></div></div><p><strong class="userinput"><code>change patt with t</code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>Each subterm matched by the pattern must be convertible
with the term <span><strong class="command">t</strong></span> disambiguated in the context
of the matched subterm.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It replaces the subterms of the current sequent matched by
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>clear id</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_auto.html" title="auto [depth=nat] [width=nat] [paramodulation] [full]" /><link rel="next" href="tac_clearbody.html" title="clearbody id" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">clear id</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_auto.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_clearbody.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="tac_clear"></a>clear <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span></h2></div></div></div><p><strong class="userinput"><code>clear H</code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>clear id</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 User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_auto.html" title="auto [depth=nat] [width=nat] [paramodulation] [full]" /><link rel="next" href="tac_clearbody.html" title="clearbody id" /></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">clear id</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_auto.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_clearbody.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="tac_clear"></a>clear <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span></h2></div></div></div><p><strong class="userinput"><code>clear H</code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p><span><strong class="command">H</strong></span> must be an hypothesis of the
current sequent to prove.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It hides the hypothesis <span><strong class="command">H</strong></span> from the
current sequent.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>None</p></dd></dl></div><p>
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>clearbody id</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_clear.html" title="clear id" /><link rel="next" href="tac_change.html" title="change <pattern> with sterm" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">clearbody id</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_clear.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_change.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="tac_clearbody"></a>clearbody <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span></h2></div></div></div><p><strong class="userinput"><code>clearbody H</code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>clearbody id</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 User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_clear.html" title="clear id" /><link rel="next" href="tac_change.html" title="change <pattern> with sterm" /></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">clearbody id</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_clear.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_change.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="tac_clearbody"></a>clearbody <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span></h2></div></div></div><p><strong class="userinput"><code>clearbody H</code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p><span><strong class="command">H</strong></span> must be an hypothesis of the
current sequent to prove.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It hides the definiens of a definition in the current
sequent context. Thus the definition becomes an hypothesis.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>None.</p></dd></dl></div><p>
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>constructor nat</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_change.html" title="change <pattern> with sterm" /><link rel="next" href="tac_contradiction.html" title="contradiction" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">constructor nat</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_change.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_contradiction.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="tac_constructor"></a>constructor <span class="emphasis"><em><a href="sec_terms.html#nat">nat</a></em></span></h2></div></div></div><p><strong class="userinput"><code>constructor n</code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>constructor nat</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 User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_change.html" title="change <pattern> with sterm" /><link rel="next" href="tac_contradiction.html" title="contradiction" /></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">constructor nat</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_change.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_contradiction.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="tac_constructor"></a>constructor <span class="emphasis"><em><a href="sec_terms.html#nat">nat</a></em></span></h2></div></div></div><p><strong class="userinput"><code>constructor n</code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>The conclusion of the current sequent must be
an inductive type or the application of an inductive type with
at least <span><strong class="command">n</strong></span> constructors.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It applies the <span><strong class="command">n</strong></span>-th constructor of the
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>contradiction</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_constructor.html" title="constructor nat" /><link rel="next" href="tac_cut.html" title="cut sterm [as id]" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">contradiction</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_constructor.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_cut.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="tac_contradiction"></a>contradiction</h2></div></div></div><p><strong class="userinput"><code>contradiction </code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>contradiction</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 User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_constructor.html" title="constructor nat" /><link rel="next" href="tac_cut.html" title="cut sterm [as id]" /></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">contradiction</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_constructor.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_cut.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="tac_contradiction"></a>contradiction</h2></div></div></div><p><strong class="userinput"><code>contradiction </code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>There must be in the current context an hypothesis of type
<span><strong class="command">False</strong></span>.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It closes the current sequent by applying an hypothesis of
type <span><strong class="command">False</strong></span>.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>None</p></dd></dl></div><p>
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>cut sterm [as id]</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_contradiction.html" title="contradiction" /><link rel="next" href="tac_decompose.html" title="decompose id [id]… [<intros_spec>]" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">cut sterm [as id]</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_contradiction.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_decompose.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="tac_cut"></a>cut <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span> [as <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>]</h2></div></div></div><p><strong class="userinput"><code>cut P as H</code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>cut sterm [as id]</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 User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_contradiction.html" title="contradiction" /><link rel="next" href="tac_decompose.html" title="decompose id [id]… [<intros_spec>]" /></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">cut sterm [as id]</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_contradiction.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_decompose.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="tac_cut"></a>cut <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span> [as <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>]</h2></div></div></div><p><strong class="userinput"><code>cut P as H</code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p><span><strong class="command">P</strong></span> must have type <span><strong class="command">Prop</strong></span>.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It closes the current sequent.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>It opens two new sequents. The first one has an extra
hypothesis <span><strong class="command">H:P</strong></span>. If <span><strong class="command">H</strong></span> is
omitted, the name of the hypothesis is automatically generated.
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>decompose id [id]… [<intros_spec>]</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_cut.html" title="cut sterm [as id]" /><link rel="next" href="tac_discriminate.html" title="discriminate sterm" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">decompose id [id]… [<intros_spec>]</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_cut.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_discriminate.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="tac_decompose"></a>decompose <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span> [<span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>]… [<intros_spec>]</h2></div></div></div><p><strong class="userinput"><code>decompose ???</code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>decompose id [id]… [<intros_spec>]</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 User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_cut.html" title="cut sterm [as id]" /><link rel="next" href="tac_discriminate.html" title="discriminate sterm" /></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">decompose id [id]… [<intros_spec>]</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_cut.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_discriminate.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="tac_decompose"></a>decompose <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span> [<span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>]… [<intros_spec>]</h2></div></div></div><p><strong class="userinput"><code>decompose ???</code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>TODO.</p></dd><dt><span class="term">Action:</span></dt><dd><p>TODO.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>TODO.</p></dd></dl></div><p>
</p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_cut.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_discriminate.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">cut sterm [as id] </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> discriminate sterm</td></tr></table></div></body></html>
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>discriminate sterm</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_decompose.html" title="decompose id [id]… [<intros_spec>]" /><link rel="next" href="tac_elim.html" title="elim sterm [using sterm] [<intros_spec>]" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">discriminate sterm</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_decompose.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_elim.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="tac_discriminate"></a>discriminate <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span></h2></div></div></div><p><strong class="userinput"><code>discriminate p</code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>discriminate sterm</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 User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_decompose.html" title="decompose id [id]… [<intros_spec>]" /><link rel="next" href="tac_elim.html" title="elim sterm [using sterm] [<intros_spec>]" /></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">discriminate sterm</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_decompose.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_elim.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="tac_discriminate"></a>discriminate <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span></h2></div></div></div><p><strong class="userinput"><code>discriminate p</code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p><span><strong class="command">p</strong></span> must have type <span><strong class="command">K t<sub>1</sub> ... t<sub>n</sub> = K' t'<sub>1</sub> ... t'<sub>m</sub></strong></span> where <span><strong class="command">K</strong></span> and <span><strong class="command">K'</strong></span> must be different constructors of the same inductive type and each argument list can be empty if
its constructor takes no arguments.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It closes the current sequent by proving the absurdity of
<span><strong class="command">p</strong></span>.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>None.</p></dd></dl></div><p>
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>elim sterm [using sterm] [<intros_spec>]</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_discriminate.html" title="discriminate sterm" /><link rel="next" href="tac_elimType.html" title="elimType sterm [using sterm] [<intros_spec>]" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">elim sterm [using sterm] [<intros_spec>]</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_discriminate.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_elimType.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="tac_elim"></a>elim <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span> [using <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span>] [<intros_spec>]</h2></div></div></div><p><strong class="userinput"><code>elim t using th hyps</code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>elim sterm [using sterm] [<intros_spec>]</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 User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_discriminate.html" title="discriminate sterm" /><link rel="next" href="tac_elimType.html" title="elimType sterm [using sterm] [<intros_spec>]" /></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">elim sterm [using sterm] [<intros_spec>]</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_discriminate.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_elimType.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="tac_elim"></a>elim <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span> [using <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span>] [<intros_spec>]</h2></div></div></div><p><strong class="userinput"><code>elim t using th hyps</code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p><span><strong class="command">t</strong></span> must inhabit an inductive type and
<span><strong class="command">th</strong></span> must be an elimination principle for that
inductive type. If <span><strong class="command">th</strong></span> is omitted the appropriate
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>elimType sterm [using sterm] [<intros_spec>]</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_elim.html" title="elim sterm [using sterm] [<intros_spec>]" /><link rel="next" href="tac_exact.html" title="exact sterm" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">elimType sterm [using sterm] [<intros_spec>]</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_elim.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_exact.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="tac_elimType"></a>elimType <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span> [using <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span>] [<intros_spec>]</h2></div></div></div><p><strong class="userinput"><code>elimType T using th hyps</code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>elimType sterm [using sterm] [<intros_spec>]</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 User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_elim.html" title="elim sterm [using sterm] [<intros_spec>]" /><link rel="next" href="tac_exact.html" title="exact sterm" /></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">elimType sterm [using sterm] [<intros_spec>]</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_elim.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_exact.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="tac_elimType"></a>elimType <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span> [using <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span>] [<intros_spec>]</h2></div></div></div><p><strong class="userinput"><code>elimType T using th hyps</code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p><span><strong class="command">T</strong></span> must be an inductive type.</p></dd><dt><span class="term">Action:</span></dt><dd><p>TODO (severely bugged now).</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>TODO</p></dd></dl></div><p>
</p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_elim.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_exact.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">elim sterm [using sterm] [<intros_spec>] </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> exact sterm</td></tr></table></div></body></html>
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>exact sterm</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_elimType.html" title="elimType sterm [using sterm] [<intros_spec>]" /><link rel="next" href="tac_exists.html" title="exists" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">exact sterm</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_elimType.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_exists.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="tac_exact"></a>exact <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span></h2></div></div></div><p><strong class="userinput"><code>exact p</code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>exact sterm</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 User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_elimType.html" title="elimType sterm [using sterm] [<intros_spec>]" /><link rel="next" href="tac_exists.html" title="exists" /></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">exact sterm</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_elimType.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_exists.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="tac_exact"></a>exact <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span></h2></div></div></div><p><strong class="userinput"><code>exact p</code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>The type of <span><strong class="command">p</strong></span> must be convertible
with the conclusion of the current sequent.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It closes the current sequent using <span><strong class="command">p</strong></span>.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>None.</p></dd></dl></div><p>
</p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_elimType.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_exists.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">elimType sterm [using sterm] [<intros_spec>] </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> exists</td></tr></table></div></body></html>
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>exists</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_exact.html" title="exact sterm" /><link rel="next" href="tac_fail.html" title="fail " /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">exists</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_exact.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_fail.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="tac_exists"></a>exists</h2></div></div></div><p><strong class="userinput"><code>exists </code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>exists</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 User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_exact.html" title="exact sterm" /><link rel="next" href="tac_fail.html" title="fail " /></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">exists</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_exact.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_fail.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="tac_exists"></a>exists</h2></div></div></div><p><strong class="userinput"><code>exists </code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>The conclusion of the current sequent must be
an inductive type or the application of an inductive type
with at least one constructor.</p></dd><dt><span class="term">Action:</span></dt><dd><p>Equivalent to <span><strong class="command">constructor 1</strong></span>.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>It opens a new sequent for each premise of the first
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>fail </title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_exists.html" title="exists" /><link rel="next" href="tac_fold.html" title="fold <reduction_kind> sterm <pattern>" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">fail </th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_exists.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_fold.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="tac_fail"></a>fail </h2></div></div></div><p><strong class="userinput"><code>fail</code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>fail </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 User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_exists.html" title="exists" /><link rel="next" href="tac_fold.html" title="fold <reduction_kind> sterm <pattern>" /></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">fail </th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_exists.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_fold.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="tac_fail"></a>fail </h2></div></div></div><p><strong class="userinput"><code>fail</code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>None.</p></dd><dt><span class="term">Action:</span></dt><dd><p>This tactic always fail.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>N.A.</p></dd></dl></div><p>
</p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_exists.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_fold.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">exists </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> fold <reduction_kind> sterm <pattern></td></tr></table></div></body></html>
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>fold <reduction_kind> sterm <pattern></title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_fail.html" title="fail " /><link rel="next" href="tac_fourier.html" title="fourier" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">fold <reduction_kind> sterm <pattern></th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_fail.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_fourier.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="tac_fold"></a>fold <reduction_kind> <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span> <pattern></h2></div></div></div><p><strong class="userinput"><code>fold red t patt</code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>fold <reduction_kind> sterm <pattern></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 User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_fail.html" title="fail " /><link rel="next" href="tac_fourier.html" title="fourier" /></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">fold <reduction_kind> sterm <pattern></th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_fail.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_fourier.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="tac_fold"></a>fold <reduction_kind> <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span> <pattern></h2></div></div></div><p><strong class="userinput"><code>fold red t patt</code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>The pattern must not specify the wanted term.</p></dd><dt><span class="term">Action:</span></dt><dd><p>First of all it locates all the subterms matched by
<span><strong class="command">patt</strong></span>. In the context of each matched subterm
it disambiguates the term <span><strong class="command">t</strong></span> and reduces it
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>fourier</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_fold.html" title="fold <reduction_kind> sterm <pattern>" /><link rel="next" href="tac_fwd.html" title="fwd id [<ident list>]" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">fourier</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_fold.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_fwd.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="tac_fourier"></a>fourier</h2></div></div></div><p><strong class="userinput"><code>fourier </code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>fourier</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 User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_fold.html" title="fold <reduction_kind> sterm <pattern>" /><link rel="next" href="tac_fwd.html" title="fwd id [<ident list>]" /></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">fourier</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_fold.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_fwd.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="tac_fourier"></a>fourier</h2></div></div></div><p><strong class="userinput"><code>fourier </code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>The conclusion of the current sequent must be a linear
inequation over real numbers taken from standard library of
Coq. Moreover the inequations in the hypotheses must imply the
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>fwd id [<ident list>]</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_fourier.html" title="fourier" /><link rel="next" href="tac_generalize.html" title="generalize <pattern> [as id]" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">fwd id [<ident list>]</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_fourier.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_generalize.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="tac_fwd"></a>fwd <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span> [<ident list>]</h2></div></div></div><p><strong class="userinput"><code>fwd ...TODO</code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>fwd id [<ident list>]</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 User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_fourier.html" title="fourier" /><link rel="next" href="tac_generalize.html" title="generalize <pattern> [as id]" /></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">fwd id [<ident list>]</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_fourier.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_generalize.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="tac_fwd"></a>fwd <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span> [<ident list>]</h2></div></div></div><p><strong class="userinput"><code>fwd ...TODO</code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>TODO.</p></dd><dt><span class="term">Action:</span></dt><dd><p>TODO.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>TODO.</p></dd></dl></div><p>
</p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_fourier.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_generalize.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">fourier </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> generalize <pattern> [as id]</td></tr></table></div></body></html>
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>generalize <pattern> [as id]</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_fwd.html" title="fwd id [<ident list>]" /><link rel="next" href="tac_id.html" title="id" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">generalize <pattern> [as id]</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_fwd.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_id.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="tac_generalize"></a>generalize <pattern> [as <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>]</h2></div></div></div><p><strong class="userinput"><code>generalize patt as H</code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>generalize <pattern> [as id]</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 User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_fwd.html" title="fwd id [<ident list>]" /><link rel="next" href="tac_id.html" title="id" /></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">generalize <pattern> [as id]</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_fwd.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_id.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="tac_generalize"></a>generalize <pattern> [as <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>]</h2></div></div></div><p><strong class="userinput"><code>generalize patt as H</code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>All the terms matched by <span><strong class="command">patt</strong></span> must be
convertible and close in the context of the current sequent.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It closes the current sequent by applying a stronger
lemma that is proved using the new generated sequent.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>It opens a new sequent where the current sequent conclusion
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>id</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_generalize.html" title="generalize <pattern> [as id]" /><link rel="next" href="tac_injection.html" title="injection sterm" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">id</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_generalize.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_injection.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="tac_id"></a>id</h2></div></div></div><p><strong class="userinput"><code>id </code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>id</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 User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_generalize.html" title="generalize <pattern> [as id]" /><link rel="next" href="tac_injection.html" title="injection sterm" /></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">id</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_generalize.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_injection.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="tac_id"></a>id</h2></div></div></div><p><strong class="userinput"><code>id </code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>None.</p></dd><dt><span class="term">Action:</span></dt><dd><p>This identity tactic does nothing without failing.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>None.</p></dd></dl></div><p>
</p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_generalize.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_injection.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">generalize <pattern> [as id] </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> injection sterm</td></tr></table></div></body></html>
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>injection sterm</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_id.html" title="id" /><link rel="next" href="tac_intro.html" title="intro [id]" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">injection sterm</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_id.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_intro.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="tac_injection"></a>injection <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span></h2></div></div></div><p><strong class="userinput"><code>injection p</code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>injection sterm</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 User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_id.html" title="id" /><link rel="next" href="tac_intro.html" title="intro [id]" /></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">injection sterm</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_id.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_intro.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="tac_injection"></a>injection <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span></h2></div></div></div><p><strong class="userinput"><code>injection p</code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p><span><strong class="command">p</strong></span> must have type <span><strong class="command">K t<sub>1</sub> ... t<sub>n</sub> = K t'<sub>1</sub> ... t'<sub>n</sub></strong></span> where both argument lists are empty if
<span><strong class="command">K</strong></span> takes no arguments.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It derives new hypotheses by injectivity of
<span><strong class="command">K</strong></span>.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>The new sequent to prove is equal to the current sequent
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>intro [id]</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_injection.html" title="injection sterm" /><link rel="next" href="tac_intros.html" title="intros <intros_spec>" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">intro [id]</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_injection.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_intros.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="tac_intro"></a>intro [<span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>]</h2></div></div></div><p><strong class="userinput"><code>intro H</code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>intro [id]</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 User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_injection.html" title="injection sterm" /><link rel="next" href="tac_intros.html" title="intros <intros_spec>" /></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">intro [id]</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_injection.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_intros.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="tac_intro"></a>intro [<span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>]</h2></div></div></div><p><strong class="userinput"><code>intro H</code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>The conclusion of the sequent to prove must be an implication
or a universal quantification.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It applies the right introduction rule for implication,
closing the current sequent.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>It opens a new sequent to prove adding to the hypothesis
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>intros <intros_spec></title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_intro.html" title="intro [id]" /><link rel="next" href="tac_inversion.html" title="inversion sterm" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">intros <intros_spec></th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_intro.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_inversion.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="tac_intros"></a>intros <intros_spec></h2></div></div></div><p><strong class="userinput"><code>intros hyps</code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>intros <intros_spec></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 User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_intro.html" title="intro [id]" /><link rel="next" href="tac_inversion.html" title="inversion sterm" /></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">intros <intros_spec></th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_intro.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_inversion.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="tac_intros"></a>intros <intros_spec></h2></div></div></div><p><strong class="userinput"><code>intros hyps</code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>If <span><strong class="command">hyps</strong></span> specifies a number of hypotheses
to introduce, then the conclusion of the current sequent must
be formed by at least that number of imbricated implications
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>inversion sterm</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_intros.html" title="intros <intros_spec>" /><link rel="next" href="tac_lapply.html" title="lapply [depth=nat] sterm [to <term list>] [using id]" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">inversion sterm</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_intros.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_lapply.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="tac_inversion"></a>inversion <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span></h2></div></div></div><p><strong class="userinput"><code>inversion t</code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>inversion sterm</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 User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_intros.html" title="intros <intros_spec>" /><link rel="next" href="tac_lapply.html" title="lapply [depth=nat] sterm [to <term list>] [using id]" /></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">inversion sterm</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_intros.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_lapply.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="tac_inversion"></a>inversion <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span></h2></div></div></div><p><strong class="userinput"><code>inversion t</code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>The type of the term <span><strong class="command">t</strong></span> must be an inductive
type or the application of an inductive type.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It proceeds by cases on <span><strong class="command">t</strong></span> paying attention
to the constraints imposed by the actual "right arguments"
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>lapply [depth=nat] sterm [to <term list>] [using id]</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_inversion.html" title="inversion sterm" /><link rel="next" href="tac_left.html" title="left" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">lapply [depth=nat] sterm [to <term list>] [using id]</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_inversion.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_left.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="tac_lapply"></a>lapply [depth=<span class="emphasis"><em><a href="sec_terms.html#nat">nat</a></em></span>] <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span> [to <term list>] [using <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>]</h2></div></div></div><p><strong class="userinput"><code>lapply ???</code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>lapply [depth=nat] sterm [to <term list>] [using id]</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 User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_inversion.html" title="inversion sterm" /><link rel="next" href="tac_left.html" title="left" /></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">lapply [depth=nat] sterm [to <term list>] [using id]</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_inversion.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_left.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="tac_lapply"></a>lapply [depth=<span class="emphasis"><em><a href="sec_terms.html#nat">nat</a></em></span>] <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span> [to <term list>] [using <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span>]</h2></div></div></div><p><strong class="userinput"><code>lapply ???</code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>TODO.</p></dd><dt><span class="term">Action:</span></dt><dd><p>TODO.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>TODO.</p></dd></dl></div><p>
</p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_inversion.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_left.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">inversion sterm </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> left</td></tr></table></div></body></html>
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>left</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_lapply.html" title="lapply [depth=nat] sterm [to <term list>] [using id]" /><link rel="next" href="tac_letin.html" title="letin id ≝ sterm" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">left</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_lapply.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_letin.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="tac_left"></a>left</h2></div></div></div><p><strong class="userinput"><code>left </code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>left</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 User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_lapply.html" title="lapply [depth=nat] sterm [to <term list>] [using id]" /><link rel="next" href="tac_letin.html" title="letin id ≝ sterm" /></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">left</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_lapply.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_letin.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="tac_left"></a>left</h2></div></div></div><p><strong class="userinput"><code>left </code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>The conclusion of the current sequent must be
an inductive type or the application of an inductive type
with at least one constructor.</p></dd><dt><span class="term">Action:</span></dt><dd><p>Equivalent to <span><strong class="command">constructor 1</strong></span>.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>It opens a new sequent for each premise of the first
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>letin id ≝ sterm</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_left.html" title="left" /><link rel="next" href="tac_normalize.html" title="normalize <pattern>" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">letin id ≝ sterm</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_left.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_normalize.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="tac_letin"></a>letin <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span> ≝ <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span></h2></div></div></div><p><strong class="userinput"><code>letin x ≝ t</code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>letin id ≝ sterm</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 User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_left.html" title="left" /><link rel="next" href="tac_normalize.html" title="normalize <pattern>" /></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">letin id ≝ sterm</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_left.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_normalize.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="tac_letin"></a>letin <span class="emphasis"><em><a href="sec_terms.html#id">id</a></em></span> ≝ <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span></h2></div></div></div><p><strong class="userinput"><code>letin x ≝ t</code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>None.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It adds to the context of the current sequent to prove a new
definition <span><strong class="command">x ≝ t</strong></span>.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>None.</p></dd></dl></div><p>
</p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_left.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_normalize.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">left </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> normalize <pattern></td></tr></table></div></body></html>
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>normalize <pattern></title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_letin.html" title="letin id ≝ sterm" /><link rel="next" href="tac_paramodulation.html" title="paramodulation <pattern>" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">normalize <pattern></th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_letin.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_paramodulation.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="tac_normalize"></a>normalize <pattern></h2></div></div></div><p><strong class="userinput"><code>normalize patt</code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>normalize <pattern></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 User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_letin.html" title="letin id ≝ sterm" /><link rel="next" href="tac_paramodulation.html" title="paramodulation <pattern>" /></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">normalize <pattern></th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_letin.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_paramodulation.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="tac_normalize"></a>normalize <pattern></h2></div></div></div><p><strong class="userinput"><code>normalize patt</code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>None.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It replaces all the terms matched by <span><strong class="command">patt</strong></span>
with their βδιζ-normal form.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>None.</p></dd></dl></div><p>
</p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_letin.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_paramodulation.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">letin id ≝ sterm </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> paramodulation <pattern></td></tr></table></div></body></html>
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>paramodulation <pattern></title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_normalize.html" title="normalize <pattern>" /><link rel="next" href="tac_reduce.html" title="reduce <pattern>" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">paramodulation <pattern></th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_normalize.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_reduce.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="tac_paramodulation"></a>paramodulation <pattern></h2></div></div></div><p><strong class="userinput"><code>paramodulation patt</code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>paramodulation <pattern></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 User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_normalize.html" title="normalize <pattern>" /><link rel="next" href="tac_reduce.html" title="reduce <pattern>" /></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">paramodulation <pattern></th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_normalize.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_reduce.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="tac_paramodulation"></a>paramodulation <pattern></h2></div></div></div><p><strong class="userinput"><code>paramodulation patt</code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>TODO.</p></dd><dt><span class="term">Action:</span></dt><dd><p>TODO.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>TODO.</p></dd></dl></div><p>
</p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_normalize.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_reduce.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">normalize <pattern> </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> reduce <pattern></td></tr></table></div></body></html>
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>reduce <pattern></title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_paramodulation.html" title="paramodulation <pattern>" /><link rel="next" href="tac_reflexivity.html" title="reflexivity" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">reduce <pattern></th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_paramodulation.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_reflexivity.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="tac_reduce"></a>reduce <pattern></h2></div></div></div><p><strong class="userinput"><code>reduce patt</code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>reduce <pattern></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 User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_paramodulation.html" title="paramodulation <pattern>" /><link rel="next" href="tac_reflexivity.html" title="reflexivity" /></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">reduce <pattern></th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_paramodulation.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_reflexivity.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="tac_reduce"></a>reduce <pattern></h2></div></div></div><p><strong class="userinput"><code>reduce patt</code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>None.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It replaces all the terms matched by <span><strong class="command">patt</strong></span>
with their βδιζ-normal form.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>None.</p></dd></dl></div><p>
</p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_paramodulation.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_reflexivity.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">paramodulation <pattern> </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> reflexivity</td></tr></table></div></body></html>
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>reflexivity</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_reduce.html" title="reduce <pattern>" /><link rel="next" href="tac_replace.html" title="replace <pattern> with sterm" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">reflexivity</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_reduce.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_replace.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="tac_reflexivity"></a>reflexivity</h2></div></div></div><p><strong class="userinput"><code>reflexivity </code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>reflexivity</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 User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_reduce.html" title="reduce <pattern>" /><link rel="next" href="tac_replace.html" title="replace <pattern> with sterm" /></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">reflexivity</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_reduce.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_replace.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="tac_reflexivity"></a>reflexivity</h2></div></div></div><p><strong class="userinput"><code>reflexivity </code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>The conclusion of the current sequent must be
<span><strong class="command">t=t</strong></span> for some term <span><strong class="command">t</strong></span></p></dd><dt><span class="term">Action:</span></dt><dd><p>It closes the current sequent by reflexivity
of equality.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>None.</p></dd></dl></div><p>
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>replace <pattern> with sterm</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_reflexivity.html" title="reflexivity" /><link rel="next" href="tac_rewrite.html" title="rewrite [<|>] sterm <pattern>" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">replace <pattern> with sterm</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_reflexivity.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_rewrite.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="tac_replace"></a>replace <pattern> with <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span></h2></div></div></div><p><strong class="userinput"><code>change patt with t</code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>replace <pattern> with sterm</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 User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_reflexivity.html" title="reflexivity" /><link rel="next" href="tac_rewrite.html" title="rewrite [<|>] sterm <pattern>" /></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">replace <pattern> with sterm</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_reflexivity.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_rewrite.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="tac_replace"></a>replace <pattern> with <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span></h2></div></div></div><p><strong class="userinput"><code>change patt with t</code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>None.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It replaces the subterms of the current sequent matched by
<span><strong class="command">patt</strong></span> with the new term <span><strong class="command">t</strong></span>.
For each subterm matched by the pattern, <span><strong class="command">t</strong></span> is
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>rewrite [<|>] sterm <pattern></title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_replace.html" title="replace <pattern> with sterm" /><link rel="next" href="tac_right.html" title="right" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">rewrite [<|>] sterm <pattern></th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_replace.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_right.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="tac_rewrite"></a>rewrite [<|>] <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span> <pattern></h2></div></div></div><p><strong class="userinput"><code>rewrite dir p patt</code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>rewrite [<|>] sterm <pattern></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 User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_replace.html" title="replace <pattern> with sterm" /><link rel="next" href="tac_right.html" title="right" /></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">rewrite [<|>] sterm <pattern></th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_replace.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_right.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="tac_rewrite"></a>rewrite [<|>] <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span> <pattern></h2></div></div></div><p><strong class="userinput"><code>rewrite dir p patt</code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p><span><strong class="command">p</strong></span> must be the proof of an equality,
possibly under some hypotheses.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It looks in every term matched by <span><strong class="command">patt</strong></span>
for all the occurrences of the
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>right</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_rewrite.html" title="rewrite [<|>] sterm <pattern>" /><link rel="next" href="tac_ring.html" title="ring" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">right</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_rewrite.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_ring.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="tac_right"></a>right</h2></div></div></div><p><strong class="userinput"><code>right </code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>right</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 User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_rewrite.html" title="rewrite [<|>] sterm <pattern>" /><link rel="next" href="tac_ring.html" title="ring" /></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">right</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_rewrite.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_ring.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="tac_right"></a>right</h2></div></div></div><p><strong class="userinput"><code>right </code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>The conclusion of the current sequent must be
an inductive type or the application of an inductive type with
at least two constructors.</p></dd><dt><span class="term">Action:</span></dt><dd><p>Equivalent to <span><strong class="command">constructor 2</strong></span>.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>It opens a new sequent for each premise of the second
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>ring</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_right.html" title="right" /><link rel="next" href="tac_simplify.html" title="simplify <pattern>" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">ring</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_right.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_simplify.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="tac_ring"></a>ring</h2></div></div></div><p><strong class="userinput"><code>ring </code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>ring</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 User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_right.html" title="right" /><link rel="next" href="tac_simplify.html" title="simplify <pattern>" /></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">ring</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_right.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_simplify.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="tac_ring"></a>ring</h2></div></div></div><p><strong class="userinput"><code>ring </code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>The conclusion of the current sequent must be an
equality over Coq's real numbers that can be proved using
the ring properties of the real numbers only.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It closes the current sequent veryfying the equality by
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>simplify <pattern></title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_ring.html" title="ring" /><link rel="next" href="tac_split.html" title="split" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">simplify <pattern></th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_ring.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_split.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="tac_simplify"></a>simplify <pattern></h2></div></div></div><p><strong class="userinput"><code>simplify patt</code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>simplify <pattern></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 User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_ring.html" title="ring" /><link rel="next" href="tac_split.html" title="split" /></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">simplify <pattern></th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_ring.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_split.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="tac_simplify"></a>simplify <pattern></h2></div></div></div><p><strong class="userinput"><code>simplify patt</code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>None.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It replaces all the terms matched by <span><strong class="command">patt</strong></span>
with other convertible terms that are supposed to be simpler.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>None.</p></dd></dl></div><p>
</p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_ring.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_split.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">ring </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> split</td></tr></table></div></body></html>
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>split</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_simplify.html" title="simplify <pattern>" /><link rel="next" href="tac_symmetry.html" title="symmetry" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">split</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_simplify.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_symmetry.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="tac_split"></a>split</h2></div></div></div><p><strong class="userinput"><code>split </code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>split</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 User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_simplify.html" title="simplify <pattern>" /><link rel="next" href="tac_symmetry.html" title="symmetry" /></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">split</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_simplify.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_symmetry.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="tac_split"></a>split</h2></div></div></div><p><strong class="userinput"><code>split </code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>The conclusion of the current sequent must be
an inductive type or the application of an inductive type with
at least one constructor.</p></dd><dt><span class="term">Action:</span></dt><dd><p>Equivalent to <span><strong class="command">constructor 1</strong></span>.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>It opens a new sequent for each premise of the first
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>symmetry</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_split.html" title="split" /><link rel="next" href="tac_transitivity.html" title="transitivity sterm" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">symmetry</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_split.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_transitivity.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="tac_symmetry"></a>symmetry</h2></div></div></div><p>The tactic <span><strong class="command">symmetry</strong></span> </p><p><strong class="userinput"><code>symmetry </code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>symmetry</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 User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_split.html" title="split" /><link rel="next" href="tac_transitivity.html" title="transitivity sterm" /></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">symmetry</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_split.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_transitivity.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="tac_symmetry"></a>symmetry</h2></div></div></div><p>The tactic <span><strong class="command">symmetry</strong></span> </p><p><strong class="userinput"><code>symmetry </code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>The conclusion of the current proof must be an equality.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It swaps the two sides of the equalityusing the symmetric
property.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>None.</p></dd></dl></div><p>
</p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_split.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_transitivity.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">split </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> transitivity sterm</td></tr></table></div></body></html>
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>transitivity sterm</title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_symmetry.html" title="symmetry" /><link rel="next" href="tac_unfold.html" title="unfold [sterm] <pattern>" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">transitivity sterm</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_symmetry.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_unfold.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="tac_transitivity"></a>transitivity <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span></h2></div></div></div><p><strong class="userinput"><code>transitivity t</code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>transitivity sterm</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 User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_symmetry.html" title="symmetry" /><link rel="next" href="tac_unfold.html" title="unfold [sterm] <pattern>" /></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">transitivity sterm</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_symmetry.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_unfold.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="tac_transitivity"></a>transitivity <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span></h2></div></div></div><p><strong class="userinput"><code>transitivity t</code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>The conclusion of the current proof must be an equality.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It closes the current sequent by transitivity of the equality.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>It opens two new sequents <span><strong class="command">l=t</strong></span> and
<span><strong class="command">t=r</strong></span> where <span><strong class="command">l</strong></span> and <span><strong class="command">r</strong></span> are the left and right hand side of the equality in the conclusion of
the current sequent to prove.</p></dd></dl></div><p>
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>unfold [sterm] <pattern></title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_transitivity.html" title="transitivity sterm" /><link rel="next" href="tac_whd.html" title="whd <pattern>" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">unfold [sterm] <pattern></th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_transitivity.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_whd.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="tac_unfold"></a>unfold [<span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span>] <pattern></h2></div></div></div><p><strong class="userinput"><code>unfold t patt</code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>unfold [sterm] <pattern></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 User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_transitivity.html" title="transitivity sterm" /><link rel="next" href="tac_whd.html" title="whd <pattern>" /></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">unfold [sterm] <pattern></th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_transitivity.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_whd.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="tac_unfold"></a>unfold [<span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span>] <pattern></h2></div></div></div><p><strong class="userinput"><code>unfold t patt</code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>None.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It finds all the occurrences of <span><strong class="command">t</strong></span>
(possibly applied to arguments) in the subterms matched by
<span><strong class="command">patt</strong></span>. Then it δ-expands each occurrence,
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!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>whd <pattern></title><
meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_unfold.html" title="unfold [sterm] <pattern>" /><link rel="next" href="sec_tacticals.html" title="Chapter 7. Tacticals" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">whd <pattern></th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_unfold.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="sec_tacticals.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="tac_whd"></a>whd <pattern></h2></div></div></div><p><strong class="userinput"><code>whd patt</code></strong></p><p>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>whd <pattern></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 User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_unfold.html" title="unfold [sterm] <pattern>" /><link rel="next" href="sec_tacticals.html" title="Chapter 7. Tacticals" /></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">whd <pattern></th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_unfold.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="sec_tacticals.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="tac_whd"></a>whd <pattern></h2></div></div></div><p><strong class="userinput"><code>whd patt</code></strong></p><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>None.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It replaces all the terms matched by <span><strong class="command">patt</strong></span>
with their βδιζ-weak-head normal form.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>None.</p></dd></dl></div><p>
</p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_unfold.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="sec_tacticals.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">unfold [sterm] <pattern> </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> Chapter 7. Tacticals</td></tr></table></div></body></html>
projects / helm.git / commitdiff