Matita HomeMatita HomeTable of Contents
To describe syntax in this manual we use the following conventions:
Non terminal symbols are emphasized and have a link to their definition. E.g.: term
Terminal symbols are in bold. E.g.: theorem
Optional sequences of elements are put in square brackets. E.g.: [in term]
Alternatives are put in square brakets and they are separated by vertical bars. E.g.: [<|>]
Repetitions of a sequence of elements are given by putting the sequence in square brackets, that are followed by three dots. The empty sequence is a valid repetition. E.g.: [and term]…
Characters belonging to a set of characters are given by listing the set elements in square brackets. Hyphens are used to specify ranges of characters in the set. E.g.: [a-zA-Z0-9_-]
Table 4.2. id
| id | ::= | 〈〈any sequence of letters, underscores or valid XML digits prefixed by a latin letter ([a-zA-Z]) and post-fixed by a possible empty sequence of decorators ([?'`])〉〉 |
Table 4.9. Terms
| term | ::= | sterm | simple or delimited term |
| | | term term | application | |
| | | λargs.term | λ-abstraction | |
| | | Πargs.term | dependent product meant to define a datatype | |
| | | ∀args.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 rec_def | (co)recursive definitions | |
| [and rec_def]… | |||
| in term | |||
| | | … | user provided notation | |
| rec_def | ::= | id [id|_|(id[,id]… :term)]… | |
| [on id] [: term] ≝ term] |
Table 4.10. Simple terms
| sterm | ::= | (term) | |
| | | id[\subst[ id≔term [;id≔term]… ]] | identifier with optional explicit named substitution | |
| | | uri | a qualified reference | |
| | | Prop | the impredicative sort of propositions | |
| | | Set | the impredicate sort of datatypes | |
| | | CProp | one fixed predicative sort of constructive propositions | |
| | | Type | one predicative sort of datatypes | |
| | | ? | implicit argument | |
| | | ?n [[ [_|term]… ]] | metavariable | |
| | | match term [ in id ] [ return term ] with | case analysis | |
| [ match_branch[|match_branch]… ] | |||
| | | (term:term) | cast | |
| | | … | user provided notation at precedence 90 |
Table 4.12. Pattern matching
| match_branch | ::= | match_pattern ⇒ term | |
| match_pattern | ::= | id | 0-ary constructor |
| | | (id id [id]…) | n-ary constructor (binds the n arguments) | |
| | | id id [id]… | n-ary constructor (binds the n arguments) | |
| | | _ | any remaining constructor (ignoring its arguments) |