Table 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.: [<|>]
Repetition of sequences of elements are given by putting the first sequence in square brackets, that are followed by three dots. E.g.: [and term]…
Table 4.4. 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 id [id|(id[,term]… :term)]… [on nat] [: term] ≝ term | (co)recursive definitions | |
| [and [id|(id[,term]… :term)]… [on nat] [: term] ≝ term]… | |||
| in term | |||
| | | … | user provided notation |
Table 4.5. 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 | |
| | | Type | one predicative sort of datatypes | |
| | | ? | implicit argument | |
| | | ?n [[ [_|term]… ]] | metavariable | |
| | | match term [ in term ] [ return term ] with | case analysis | |
| [ match_pattern ⇒ term [ | match_pattern ⇒ term ]…] | |||
| | | (term:term) | cast | |
| | | … | user provided notation at precedence 90 |
Table 4.6. Arguments
| args | ::= | _[: term] | ignored argument |
| | | (_[: term]) | ignored argument | |
| | | id[,id]…[: term] | ||
| | | (id[,id]…[: term]) |
Table 4.8. Pattern matching
| match_pattern | ::= | id | 0-ary constructor |
| | | (id id [id]…) | n-ary constructor (binds the n arguments) |