X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fhelp%2FC%2Fsec_terms.html;fp=matita%2Fmatita%2Fhelp%2FC%2Fsec_terms.html;h=151c909c88fee0a5fec06e05146d58283e9dcbf5;hb=d29fd4947ea4551f1fa078e56ed2a21b4515536f;hp=0000000000000000000000000000000000000000;hpb=a19551fd50df93951d78eea4c163d434f844047c;p=helm.git diff --git a/matita/matita/help/C/sec_terms.html b/matita/matita/help/C/sec_terms.html new file mode 100644 index 000000000..151c909c8 --- /dev/null +++ b/matita/matita/help/C/sec_terms.html @@ -0,0 +1,53 @@ + +Chapter 4. Syntax
Chapter 4. Syntax
Prev   Next

Chapter 4. Syntax

Table of Contents

Terms & co.
Lexical conventions
Terms
Definitions and declarations
axiom
definition
discriminator
inverter
TODO
(co)inductive types declaration
record
Proofs
theorem
corollary
lemma
fact
example
Tactic arguments
pattern
reduction-kind
auto-params
justification

To describe syntax in this manual we use the following conventions:

  1. Non terminal symbols are emphasized and have a link to their + definition. E.g.: term

  2. Terminal symbols are in bold. E.g.: + theorem

  3. Optional sequences of elements are put in square brackets. + E.g.: [in term]

  4. Alternatives are put in square brakets and they are + separated by vertical bars. E.g.: [<|>]

  5. 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]…

  6. 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_-]

Terms & co.

Lexical conventions

Table 4.1. qstring

qstring::="〈〈any sequence of characters excluded "〉〉" 

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.3. nat

nat::=〈〈any sequence of valid XML digits〉〉 

Table 4.4. char

char::=[a-zA-Z0-9_-] 

Table 4.5. uri-step

uri-step::=char[char]… 

Table 4.6. uri

uri::=[cic:/|theory:/]uri-step[/uri-step]….id[.id]…[#xpointer(nat/nat[/nat]…)] 

Table 4.7. csymbol

csymbol::='id 

Table 4.8. symbol

symbol::=〈〈None of the above〉〉 

Terms

+

Table 4.9. Terms

term::=stermsimple or delimited term
 |term termapplication
 |λargs.termλ-abstraction
 |Πargs.termdependent product meant to define a datatype
 |∀args.termdependent product meant to define a proposition
 |term → termnon-dependent product (logical implication or function space)
 |let [id|(id: term)] ≝ term in termlocal 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
 |uria qualified reference
 |Propthe impredicative sort of propositions
 |Setthe impredicate sort of datatypes
 |CPropone fixed predicative sort of constructive propositions
 |Typeone 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.11. Arguments

args::= + _[: term] + ignored argument
 | + (_[: term]) + ignored argument
 |id[,id]…[: term] 
 |(id[,id]…[: term]) 
args2::=id 
 |(id[,id]…: term) 


+ +

Table 4.12. Pattern matching

match_branch::=match_pattern ⇒ term 
match_pattern::=id0-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)


+

Prev   Next
Authoring Home Definitions and declarations
\ No newline at end of file