commit 00a8b5b605b5bbee814312fe52a8fd601f266c32
Author: Pranshu Sharma <pranshu@bauherren.ovh>
Date:   Tue May 20 21:11:57 2025 +1000

    Main intro file

diff --git a/intro.lean b/intro.lean
new file mode 100644
index 0000000..986b735
--- /dev/null
+++ b/intro.lean
@@ -0,0 +1,16 @@
+
+
+def hello : String := "Hello"
+
+def add1 (n : Nat) : Nat := n + 1
+
+def maximum (n : Nat) (k : Nat) : Nat :=
+  if n < k then
+    k
+  else n
+
+def PStr : Type := String
+
+def OnePlusOneIsTwo : Prop := 1 + 1 = 2
+
+theorem onePlusOneIsTwo : OnePlusOneIsTwo := rfl