You cannot select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
22 lines
1.3 KiB
Markdown
22 lines
1.3 KiB
Markdown
# 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](https://www.dm.unipi.it/github-pro/) ci fa arrivare a 180h gratuite di utilizzo al mese.
|
|
|
|
[](https://github.com/codespaces/new?skip_quickstart=true&hide_repo_select=true&ref=main&repo=698191991&machine=standardLinux32gb&location=WestEurope)
|
|
|
|
> :warning: **Achtung** :warning: 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://lean-lang.org/theorem_proving_in_lean4/
|
|
|
|
- https://lean-lang.org/lean4/doc/
|
|
|
|
- Progetto ricavato dalla repo: <https://github.com/leanprover/lean4-samples>
|