Login
De Vito, Federico
(2024)
Breve introduzione al proof assistant Lean ed alcuni esempi di codici.
[Laurea], Università di Bologna, Corso di Studio in Matematica [L-DM270], Documento ad accesso riservato.
Documenti full-text disponibili:
![[thumbnail of Thesis]](https://amslaurea.unibo.it/style/images/fileicons/application_pdf.png) |
Documento PDF (Thesis)
Full-text accessibile solo agli utenti istituzionali dell'Ateneo Disponibile con Licenza: Salvo eventuali più ampie autorizzazioni dell'autore, la tesi può essere liberamente consultata e può essere effettuato il salvataggio e la stampa di una copia per fini strettamente personali di studio, di ricerca e di insegnamento, con espresso divieto di qualunque utilizzo direttamente o indirettamente commerciale. Ogni altro diritto sul materiale è riservato Download (358kB) | Contatta l'autore |
Abstract
L'elaborato descrive il proof assistant Lean parlando della sua storia e dove viene insegnato. Viene anche spiegato il funzionamento delle dimostrazioni e delle definizioni in Lean. Infine si vedono diversi esempi presi dalla libreria del codice.
Abstract
Altri metadati
Statistica sui download
Gestione del documento:
