Come scrivere i simboli

Per inserire i simboli matematici è necessario digitare il loro nome e poi premere ALT-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.

La sintassi ∀x.P significa "per tutti gli x 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.

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).

Il linguaggio di dimostrazione di Matita

Alcuni degli esercizi seguenti richiedono di scrivere una dimostrazione. Tale dimostrazione deve essere scritta utilizzando il linguaggio di dimostrazione di Matita. Tale linguaggio è composto dai seguenti comandi, chiamati tattiche dichiarative. I comandi sono anche descritti nel manuale on-line, consultabile a partire dal menu Help/Contents sotto la voce Declarative tactics.