- Come scrivere i simboli
- =======================
-
- Per inserire i simboli matematici è necessario digitare il loro nome
- e poi premere CTRL-L. In generale i nomi dei simboli sono della forma
- '\nome', ad esempio '\equiv'. Alcuni simboli molto frequenti hanno
- dei sinonimi più comodi da digitare, per esemio ⇒ ha sia il nome
- '\Rightarrow' sia '=>'.
-
- Segue un elenco dei simboli più comuni e i loro nomi separati da virgola,
- Se sono necessari dei simboli non riportati di seguito si può visualizzare
- l'intera lista dal menù a tendina 'View ▹ TeX/UTF8 table'.
-
- * → : \to, ->
- * ⇒ : \Rightarrow, =>
- * ℕ : \naturals
- * ≝ : \def, :=
- * ≡ : \equiv
- * ∀ : \forall
-
- La sintassi '∀v.P' significa "per tutti i 'v' vale 'P'".
-
- La sintassi 'F → G' dove 'F' e 'G' sono proposizioni nel metalinguaggio
- significa "'F' implica 'G'". Attenzione, il simbolo '⇒' (usato a lezione)
- non ha lo stesso significato in Matita.
-
- La sintassi 'ℕ → ℕ' è il tipo delle funzioni che preso un numero naturale
- restituiscono un numero naturale.
-
- La sintassi di Matita
- =====================
-
- Il linguaggio di Matita si basa sul λ-calcolo CIC, la cui sintassi si
- differenzia in vari aspetti da quella che solitamente viene utilizzata
- per fare matematica, e ricorda quella di Scheme che state vedendo nel corso
- di programmazione.
-
- * applicazione
-
- Se 'f' è una funzione che si aspetta due argomenti, l'applucazione di 'f'
- agli argomenti 'x' e 'y' si scrive '(f x y)' e non 'f(x,y)'. Le parentesi
- possono essere omesse se il senso è chiaro dal contesto. In particolare
- vengono omesse quando l'applicazione è argomento di un operatore binario.
- Esempio: 'f x y + f y x' si legge '(f x y) + (f y x)'.
-
- * minimo e massimo
-
- Le funzioni 'min' e 'max' non fanno eccezione, per calcolare il
- massimo tra 'x' e 'y' si scrive '(max x y)' e non 'max{x,y}'
-
- * Le funzioni definite per ricorsione strutturale utilizzano il costrutto
- 'let rec' (ricorsione) e il costrutto 'match' (analisi per casi).
-
- Ad esempio la funzione count definita a lezione come
-