Main intro file

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