Matita V0.1.0 Manual (rev. 0)

Andrea Asperti

Claudio Sacerdoti Coen

Enrico Tassi

Stefano Zacchiroli

This manual describes version 0.1.0 of Matita.

This file is part of HELM, an Hypertextual, Electronic Library of Mathematics, developed at the Computer Science Department, University of Bologna, Italy.

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.

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.

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 this link.

Feedback

To report a bug or make a suggestion regarding the Matita application or this manual, follow the directions in the HELM Bug Tracking System Page.

Revision History
Revision Matita V0.1.0 Manual (rev. 0)February 2006 

The HELM team

Revision 04 February 2006HELM
First draft completed.

Table of Contents

1. Introduction
Features
Matita vs Coq
2. Installation
Installing from sources
Getting the source code
Requirements
Database setup
Compiling and installing
3. Getting started
How to type Unicode symbols
Browsing and searching
Browsing the library
Looking at a proof under development
Searching the library
Authoring
How to use developments
4. Syntax
Terms & co.
Lexical conventions
Terms
Definitions and declarations
axiom
definition
(co)inductive types declaration
record
Proofs
theorem
variant
lemma
fact
remark
5. Extending the syntax
Introduction
6. Tactics
absurd
apply
assumption
auto
clear
clearbody
change
constructor
contradiction
cut
decompose
discriminate
elim
elimType
exact
exists
failt
fold
fourier
fwd
generalize
id
injection
intro
intros
inversion
lapply
left
letin
normalize
paramodulation
reduce
reflexivity
change
rewrite
right
ring
simplify
split
symmetry
transitivity
unfold
whd
7. Tacticals
Introduction
8. Other commands
Introduction
9. License

List of Figures

3.1. The Developments window

List of Tables

2.1. configure command line arguments
4.1. id
4.2. nat
4.3. uri
4.4. Terms
4.5. Simple terms
4.6. Arguments
4.7. Miscellaneous arguments
4.8. Pattern matching