Matita HomeMatita HomeTable 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 or an ASCII art resembling the shape of the character. Pressing "Alt+L" or Space or Enter just after the last character of the name converts the ligature to the Unicode symbol. E.g. "\Delta" followed by Alt+L generates "Δ", while pressing Alt-L after "=>" generates "⇒"
Typing a symbol and rotating trough its equivalence class with Alt-L. E.g. pressing Alt-L after an "l" generates a "λ", while pressing Alt-L after an "→" once generates "⇉" and pressing Alt-L again generates "⇒".
The comprehensive list of symbols names or shortcuts and their equivalence classes is available clicking on the "TeX/UTF-8 table" item of the "View" menu.
There is a memory mechanism related to equivalence classes that remembers your last choice, making it the default one. For example, if you use "_" to generate "⎻" (that is the third choice, after "⎽" and "⎼"), the next time you type Alt-L after "_" you immediately get "⎻".