From c25f685f27ea3b902fce0a87fe6d9b80c9a69bc5 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 25 May 2006 14:33:13 +0000 Subject: [PATCH] More doc --- helm/software/matita/help/C/sec_terms.xml | 149 ++++++++++++++++++++-- 1 file changed, 139 insertions(+), 10 deletions(-) diff --git a/helm/software/matita/help/C/sec_terms.xml b/helm/software/matita/help/C/sec_terms.xml index 5fafcd0ac..e9402f237 100644 --- a/helm/software/matita/help/C/sec_terms.xml +++ b/helm/software/matita/help/C/sec_terms.xml @@ -2,27 +2,156 @@ - Terms, definitions, declarations and proofs + Terms, axioms, definitions, declarations and proofs Terms - &TODO; + + + + + + + <term> + ::= + <id> + identifier + + + + | + <term> <term> + application + + + + | + λ<id>[: <term>].<term> + λ-abstraction + + + + | + Π<id>[: <term>].<term> + dependent product meant to define a datatype + + + + | + ∀<id>[: <term>].<term> + dependent product meant to define a proposition + + + + | + <term> → <term> + non-dependent product (logical implication or function space) + + + + | + let [<id>|(<id>: <term>)] ≝ <term> in <term> + local definition + + + + | + let [co]rec <id> ≝ <term> in <term> + local definition + + + + | + ... + &TODO; + + + +
- - Definitions - &TODO; + + axiom <id>: <term> + axiom + axiom H: P + H is declared as an axiom that states P - - Declarations (of inductive types) - Declarations + + definition <id>[: <term>] [≝ <term>] + definition + definition f: T ≝ t + f is defined as t; + T is its type. An error is raised if the type of + t is not convertible to T. + T is inferred from t if + omitted. + t can be omitted only if T is + given. In this case Matita enters in interactive mode and + f must be defined by means of tactics. + Notice that the command is equivalent to theorem f: T ≝ t. + + + + [co]inductive <id> (of inductive types) + (co)inductive types declaration &TODO; - Proofs - &TODO; + Proofs + + theorem <id>[: <term>] [≝ <term>] + theorem + theorem f: P ≝ p + Proves a new theorem f whose thesis is + P. + If p is provided, it must be a proof term for + P. Otherwise an interactive proof is started. + P can be omitted only if the proof is not + interactive. + Proving a theorem already proved in the library is an error. + To provide an alternative name and proof for the same theorem, use + variant f: P ≝ p. + A warning is raised if the name of the theorem cannot be obtained + by mangling the name of the constants in its thesis. + Notice that the command is equivalent to definition f: T ≝ t. + + + variant <id>[: <term>] [≝ <term>] + variant + variant f: T ≝ t + Same as theorem f: T ≝ t, but it does not + complain if the theorem has already been proved. To be used to give + an alternative name or proof to a theorem. + + + lemma <id>[: <term>] [≝ <term>] + lemma + lemma f: T ≝ t + Same as theorem f: T ≝ t + + + fact <id>[: <term>] [≝ <term>] + fact + fact f: T ≝ t + Same as theorem f: T ≝ t + + + remark <id>[: <term>] [≝ <term>] + remark + remark f: T ≝ t + Same as theorem f: T ≝ t + -- 2.39.2