-(*
- 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
-
+(*DOCBEGIN
+
+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
+