Questa repo contiene un semplice progetto in Lean che può essere lanciato con un click su GitHub CodeSpace provarlo senza dover installare nulla in locale.

GitHub / GitHub Pro con Unipi

GitHub già offre 120h gratuite al mese di utilizzo di CodeSpace, inoltre Unipi con GitHub Pro ci fa arrivare a 180h gratuite di utilizzo al mese.

[![Open in GitHub Codespaces](https://github.com/codespaces/badge.svg)](https://github.com/codespaces/new?skip_quickstart=true&hide_repo_select=true&ref=main&repo=698191991&machine=basicLinux32gb&location=WestEurope)

⚠️ Achtung ⚠️

Le 120h o 180h sono "core hours" quindi con la macchina da 2 core sono complessivamente 60h o 90h effettive al mese (le opzioni sono 2 o 4 core ma già quella da 2 dovrebbe bastare). Essenzialmente conviene usare con parsimonia le ore di questi GitHub CodeSpaces.

In particolare quando si ha finito di utilizzare il codespace ricordarsi di spegnerlo dalla pagina https://github.com/codespaces, dalla lista di codespaces se c'è scritto ancora "Active" premere sui tre puntini e fare "Stop Container".

Per provare che tutto funzioni andare in ./Main.lean e verificare che si apra il pannello laterale e che mettendo il mouse sopra #eval venga mostrata la stringa Hello, World!.

Siti Utili

https://lean-lang.org/theorem_proving_in_lean4/
https://lean-lang.org/lean4/doc/
https://github.com/leanprover/lean4-samples (da cui è stato ricavato il codice per questa repo)