Antonio De Lucreziis 92d7e249ac | 1 year ago | |
---|---|---|
.devcontainer | 1 year ago | |
Prova | 1 year ago | |
.gitignore | 1 year ago | |
Main.lean | 1 year ago | |
Prova.lean | 1 year ago | |
README.md | 1 year ago | |
lakefile.lean | 1 year ago | |
lean-toolchain | 1 year ago |
README.md
Lean Codespace
Questa repo contiene un semplice progetto in Lean con preimpostato un ambiente GitHub CodeSpace per poterlo usare 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.
⚠️ Achtung ⚠️ Per non sprecare subito tutte le ore di utilizzo 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://github.com/leanprover/lean4-samples (da cui è stato ricavato il codice per questa repo)