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 ℕ → ℕ è il tipo delle funzioni unarie che preso un numero naturale restituiscono un numero naturale.

→ associa a destra. Pertanto ℕ → ℕ → ℕ è da leggersi come ℕ → (ℕ → ℕ), ovvero il tipo delle funzioni che preso un primo input restituiscono una funzione che preso un secondo input restituiscono un naturale. In altre parole, ℕ → ℕ → ℕ è il tipo delle funzioni binarie sui naturali.

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 si avvicina a quella dei più noti linguaggi di programmazione funzionale.

La sintassi dei termini (o espressioni) è grosso modo generata dalla seguente BNF:

T ::= x | y | pippo | Pluto | ... variabili e costanti (sequenze di maiuscole, minuscole, numeri) | T ... T applicazione prefissa | T SIMBOLO T applicazione infissa dove SIMBOLO è un simbolo come +, -, =, etc. | λx.T una funzione che prende in input la variabile x (o y, o z, etc.) e restituisce in output T

Un file matita è una sequenza di dichiarazioni di tipo, definizioni di funzione, definizione di funzioni per ricorsione strutturale, assiomi e teoremi.

La ratio è che Plus prende due argomenti di tipo A per darmi un A, pertanto il simbolo terminale Plus è assimilabile a una "funzione" binaria di tipo A → A → A. Essa, tuttavia, non è una vera funzione ma solamente un terminale in quanto non calcola nulla. Matita capisce che è un terminale (chiamato costruttore) in quanto è definito come uno dei casi del tipo induttivo A nella definizione di A.

Analogamente Minus prende un argomento di tipo A per dare un A ed è pertanto dichiarato di tipo A → A. Zero e One sono invece simboli terminali atomici: essi non hanno argomento e sono già di tipo A. Vengono pertanto dichiarati come avente tipo A.

Plus, Times, Minus non sono simboli infissi. Pertanto si utilizza la normale sintassi per l'applicazione. Per esempio, 0 + -1 * 0 va scritto come Plus Zero (Times (Minus One) Zero).