Matita V0.99.5 User Manual (rev. 0.99.5 )
   Next

Matita V0.99.5 User Manual (rev. 0.99.5 )

Copyright © 2006 The HELM team.

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 Chapter 10, License for more information.

Revision: 0.99.5 , 12/07/2006

Table of Contents

1. Introduction
Features
Matita vs Coq
2. Installation
Using the LiveCD
Creating the virtual machine
Sharing files with the real PC
Installing from sources
Getting the source code
Requirements
Compiling and installing
3. Getting started
How to type Unicode symbols
Browsing and searching
Browsing the library
Looking at a proof under development
Authoring
How to compile a script
The authoring interface
4. Syntax
Terms & co.
Lexical conventions
Terms
Definitions and declarations
axiom
definition
discriminator
inverter
TODO
(co)inductive types declaration
record
Proofs
theorem
corollary
lemma
fact
example
Tactic arguments
pattern
reduction-kind
auto-params
justification
5. Extending the syntax
notation
interpretation
6. Tacticals
Interactive proofs and definitions
The proof status
Tacticals
7. Tactics
Quick reference card
@
//
#
#_
##
-
%
*
>
applyS
assumption
cases
change
cut
destruct
elim
generalize
inversion
lapply
letin
normalize
whd
8. Declarative Tactics
Quick reference card
assume
suppose
letin
that is equivalent to
the thesis becomes
we need to prove
we proved
let such that
we have
we proceed by induction on
we proceed by cases on
case
by induction hypothesis we know
conclude
obtain
=
done
9. Other commands
alias
check
coercion
include
include alias
qed
qed-
unification hint
universe constraint
10. License

List of Figures

2.1. The brand new virtual machine
2.2. Mounting an ISO image
2.3. Choosing the ISO image
2.4. Choosing the ISO image
2.5. Set up a shared folder
2.6. Choosing the folder to share
2.7. Naming the shared folder
2.8. Using it from the virtual machine

List of Tables

4.1. qstring
4.2. id
4.3. nat
4.4. char
4.5. uri-step
4.6. uri
4.7. csymbol
4.8. symbol
4.9. Terms
4.10. Simple terms
4.11. Arguments
4.12. Pattern matching
4.13. pattern
4.14. path
4.15. reduction-kind
4.16. auto-params
4.17. simple-auto-param
4.18. justification
5.1. usage
5.2. associativity
5.3. notation_rhs
5.4. unparsed_ast
5.5. enriched_term
5.6. unparsed_meta
5.7. level2_meta
5.8. notation_lhs
5.9. layout
5.10. literal
5.11. interpretation_argument
5.12. interpretation_rhs
6.1. proof script
6.2. proof steps
6.3. tactics and LCF tacticals
7.1. tactics
8.1. tactics
   Next
   Chapter 1. Introduction