+ Ad esempio la funzione count definita a lezione come
+
+ count ⊤ ≝ 1
+ count (F1 ∧ F2) ≝ 1 + count F1 + count F2
+ ...
+
+ la si esprime come
+
+ let rec count F on F ≝
+ match F with
+ [ ⊤ ⇒ 1
+ | F1 ∧ F2 ⇒ 1 + count F1 + count F2
+ ...
+ ].
+
+ * Per dare la definizione ricorsiva (di un linguaggio) si usa una sintassi
+ simile a BNF. Per esempio per definire
+
+ <A> ::= <A> "+" <A> | <A> "*" <A> | "0" | "1"
+
+ si usa il seguente comando
+
+ inductive A : Type ≝
+ | Plus : A → A → A
+ | Times : A → A → A
+ | Zero : A
+ | One : A
+ .
+
+ La ratio è che 'Plus' prende due argomenti di tipo A per darmi un A,
+ mentre 'Zero' non prende nessun argomento per darmi un A. Al posto di usare
+ operatori infissi (0 + 0) la definizione crea operatori prefissi (funzioni).
+ Quindi (0+0) si scriverà come (Plus Zero Zero).
+
+*)