From c52baa34c7363fa58f81aea95bb0d72e10afdaf1 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 26 May 2006 15:14:41 +0000 Subject: [PATCH] New documentation. --- helm/software/matita/help/C/matita.xml | 6 ++ helm/software/matita/help/C/sec_commands.xml | 7 ++ .../matita/help/C/sec_gettingstarted.xml | 85 ++++++++++++++++++- helm/software/matita/help/C/sec_intro.xml | 7 +- .../matita/help/C/sec_usernotation.xml | 7 ++ 5 files changed, 110 insertions(+), 2 deletions(-) create mode 100644 helm/software/matita/help/C/sec_commands.xml create mode 100644 helm/software/matita/help/C/sec_usernotation.xml diff --git a/helm/software/matita/help/C/matita.xml b/helm/software/matita/help/C/matita.xml index 1120cb4ec..41d763c93 100644 --- a/helm/software/matita/help/C/matita.xml +++ b/helm/software/matita/help/C/matita.xml @@ -8,6 +8,9 @@ + + + @@ -156,7 +159,10 @@ &install; &gettingstarted; &terms; +&usernotation; &tactics; +&tacticals; +&othercommands; diff --git a/helm/software/matita/help/C/sec_commands.xml b/helm/software/matita/help/C/sec_commands.xml new file mode 100644 index 000000000..b1bada0fd --- /dev/null +++ b/helm/software/matita/help/C/sec_commands.xml @@ -0,0 +1,7 @@ + + + + Other commands + &TODO; + + diff --git a/helm/software/matita/help/C/sec_gettingstarted.xml b/helm/software/matita/help/C/sec_gettingstarted.xml index b7b006590..f7d435e70 100644 --- a/helm/software/matita/help/C/sec_gettingstarted.xml +++ b/helm/software/matita/help/C/sec_gettingstarted.xml @@ -3,10 +3,93 @@ 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 + 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 opzionally 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; + + + + + Authoring &TODO; - &TODO; diff --git a/helm/software/matita/help/C/sec_intro.xml b/helm/software/matita/help/C/sec_intro.xml index 169517088..a29b4960d 100644 --- a/helm/software/matita/help/C/sec_intro.xml +++ b/helm/software/matita/help/C/sec_intro.xml @@ -56,7 +56,12 @@ an extensible language of tactics; automatic implicit arguments; several ad-hoc decision procedures; - several rarely used variants for most of the tactics. + several rarely used variants for most of the tactics; + sections and local variables. To maintain compatibility + with the library of Coq, theorems defined inside sections are abstracted + by name over the section variables; their instances are explicitly + applied to actual arguments by means of explicit named + substitutions. diff --git a/helm/software/matita/help/C/sec_usernotation.xml b/helm/software/matita/help/C/sec_usernotation.xml new file mode 100644 index 000000000..92698f824 --- /dev/null +++ b/helm/software/matita/help/C/sec_usernotation.xml @@ -0,0 +1,7 @@ + + + + Extending the syntax + &TODO; + + -- 2.39.2