Matita V0.99.3 User Manual (rev. 0.99.3 )
   Next

Matita V0.99.3 User Manual (rev. 0.99.3 )

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

Revision: 0.99.3 , 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
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. Other commands
alias
check
coercion
include
include alias
qed
qed-
unification hint
universe constraint
9. 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
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
   Next
   Chapter 1. Introduction