commit d2105790281a6f4857e2e3edbdb76be33f30ab04
Author: Antonio De Lucreziis <antonio.delucreziis@gmail.com>
Date:   Fri Sep 29 13:11:59 2023 +0200

    initial commit

diff --git a/.devcontainer/Dockerfile b/.devcontainer/Dockerfile
new file mode 100644
index 0000000..cd10100
--- /dev/null
+++ b/.devcontainer/Dockerfile
@@ -0,0 +1,9 @@
+ARG VARIANT="jammy"
+FROM mcr.microsoft.com/vscode/devcontainers/base:0-${VARIANT}
+
+RUN apt-get update && apt-get install -yq build-essential nodejs npm
+
+USER vscode
+RUN echo $HOME
+RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSfL | sh -s -- --default-toolchain leanprover/lean4:stable -y
+RUN echo 'export PATH="$HOME/.elan/bin:$PATH"' >> $HOME/.profile
diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json
new file mode 100644
index 0000000..66c9583
--- /dev/null
+++ b/.devcontainer/devcontainer.json
@@ -0,0 +1,18 @@
+{
+	"name": "Ubuntu",
+	"build": {
+		"dockerfile": "Dockerfile",
+		"args": { "VARIANT": "ubuntu-22.04" }
+	},
+	"remoteUser": "vscode",
+	"features": {
+		"git": "os-provided"
+	},
+	"customizations": {
+		"vscode": {
+			"extensions": [
+				"leanprover.lean4"
+			]
+		}
+	}
+}
diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..1824d0c
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,3 @@
+/build
+/lakefile.olean
+/lake-packages/*
diff --git a/Main.lean b/Main.lean
new file mode 100644
index 0000000..fedff09
--- /dev/null
+++ b/Main.lean
@@ -0,0 +1,6 @@
+import Prova 
+
+def main : IO Unit :=
+  IO.println s!"Hello, {hello}!"
+
+#eval main
diff --git a/Prova.lean b/Prova.lean
new file mode 100644
index 0000000..be31539
--- /dev/null
+++ b/Prova.lean
@@ -0,0 +1,3 @@
+-- This module serves as the root of the `Prova` library.
+-- Import modules here that should be built as part of the library.
+import Prova.Basic
\ No newline at end of file
diff --git a/Prova/Basic.lean b/Prova/Basic.lean
new file mode 100644
index 0000000..e99d3a6
--- /dev/null
+++ b/Prova/Basic.lean
@@ -0,0 +1 @@
+def hello := "world"
\ No newline at end of file
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..399cc85
--- /dev/null
+++ b/README.md
@@ -0,0 +1,8 @@
+# Lean Codespace
+
+Progetto ricavato dalla repo: <https://github.com/leanprover/lean4-samples>
+
+## GitHub Pro con Unipi
+
+[![Open in GitHub Codespaces](https://github.com/codespaces/badge.svg)](https://github.com/codespaces/new?hide_repo_select=true&ref=main&repo=452801263&machine=standardLinux32gb&location=WestEurope)
+
diff --git a/lakefile.lean b/lakefile.lean
new file mode 100644
index 0000000..92e2815
--- /dev/null
+++ b/lakefile.lean
@@ -0,0 +1,16 @@
+import Lake
+open Lake DSL
+
+package prova where
+  -- add package configuration options here
+
+lean_lib Prova where
+  -- add library configuration options here
+
+@[default_target]
+lean_exe «prova» where
+  root := `Main
+  -- Enables the use of the Lean interpreter by the executable (e.g.,
+  -- `runFrontend`) at the expense of increased binary size on Linux.
+  -- Remove this line if you do not need such functionality.
+  supportInterpreter := true
diff --git a/lean-toolchain b/lean-toolchain
new file mode 100644
index 0000000..7638861
--- /dev/null
+++ b/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:stable