X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_gettingstarted.xml;h=5f9dda35a829d1a6ba7fc86093841f1740de8fe6;hb=871ed1c297e8c929a8c4460162e8521c9656bbc0;hp=b7b006590a39498117d0a7d267aaf6f293a66514;hpb=606b4dbe57c4ccbf4c25f3eac4576b98977885c8;p=helm.git diff --git a/helm/software/matita/help/C/sec_gettingstarted.xml b/helm/software/matita/help/C/sec_gettingstarted.xml index b7b006590..5f9dda35a 100644 --- a/helm/software/matita/help/C/sec_gettingstarted.xml +++ b/helm/software/matita/help/C/sec_gettingstarted.xml @@ -3,10 +3,95 @@ Getting started + 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. + How to type Unicode symbols - &TODO; + Unicode characters can be typed in several ways: + + Using the "Shift+Ctrl+Unicode code" standard Gnome shortcut. E.g. Shift+Ctrl+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 "⇒"). + + + + + Browsing and searching + The CIC browser is used to browse and search the library. + You can open a new CIC browser selecting "New Cic Browser" + from the "View" menu of Matita, or by pressing "F3". + The CIC browser is similar to a traditional Web browser. + + Browsing the library + To browse the library, type in the location bar the absolute URI of + the theorem, definition or library fragment you are interested in. + "cic:/" is the root of the library. Contributions developed + in Matita are under "cic:/matita"; all the others are + part of the library of Coq. + Following the hyperlinks it is possible to navigate in the Web + of mathematical notions. Proof are rendered in pseudo-natural language + and mathematical notation is used for formulae. For now, mathematical + notation must be included in the current script to be activated, but we + plan to remove this limitation. + + + Looking at a proof under development + A proof under development is not yet part of the library. + The special URI "about:proof" can be used to browse the + proof currently under development, if there is one. + The "home" button of the CIC browser sets the location bar to + "about:proof". + + + + Searching the library + The query bar of the CIC browser can be used to search the library + of Matita for theorems or definitions that match certain criteria. + The criteria is given by typing a term in the query bar and selecting + an action in the drop down menu right of it. + + Searching by name + &TODO; + + + List of lemmas that can be applied + &TODO; + + + Searching by exact match + &TODO; + + + List of elimination principles for a given type + &TODO; + + + Searching by instantiation + &TODO; + + - &TODO; + + Authoring + + How to use developments + &TODO; + +