Table of Contents
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 and search the library and how to author a proof script.
Unicode characters can be typed in several ways:
Using the "Ctrl+Shift+Unicode code" standard Gnome shortcut. E.g. Ctrl+Shift+3a9 generates "Ω".
Typing the ligature "\name" where "name" is a standard Unicode or LaTeX name for the character. Pressing "Alt+L" just after the last character of the name converts the ligature to the Unicode symbol. This operation is not required since Matita understands also the "\name" sequences. E.g. "\Omega" followed by Alt+L generates "Ω".
Typing one of the following ligatures (and optionally converting the ligature to the Unicode character has described before): ":=" (which stands for ≝); "->" (which stands for "→"); "=>" (which stands for "⇒").