From: Claudio Sacerdoti Coen Date: Thu, 25 May 2006 14:33:13 +0000 (+0000) Subject: More doc X-Git-Tag: 0.4.95@7852~1432 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=09c2feb12e84b2d2bd2e04454274b1e9e7fcfa8b;p=helm.git More doc --- diff --git a/matita/help/C/sec_terms.xml b/matita/help/C/sec_terms.xml index 5fafcd0ac..e9402f237 100644 --- a/matita/help/C/sec_terms.xml +++ b/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 +