diff --git a/dependent-types.lean b/dependent-types.lean
new file mode 100644
index 0000000..9e94fb4
--- /dev/null
+++ b/dependent-types.lean
@@ -0,0 +1,32 @@
+
+
+-- Ok, from what I understnad dependent types are kind of the type
+-- equvileant to first-class functions.  Types can be stored,
+-- returned, kinda like in zig. 
+
+-- Btw unicode is cool, reminds me of raku
+def α : Type := Nat
+-- α is a variable that stores the type
+#check α    -- > α : Type
+
+-- BTW #check is like eval but works for types
+
+-- This is a function that takes a type and returns a type
+def F : Type → Type := List
+
+#check F α
+
+def IntOrString (isInt : Bool) : Type :=
+  match isInt with
+    | false => Int
+    | true => String
+
+#check IntOrString false
+
+-- showOrReverse : (isInt : Bool) -> IntOrString isInt -> String
+def negateOrIdentity (isString : Bool) (val : IntOrString isString)  : IntOrString isString :=
+   match isString with
+    | true => val
+    | false => -val
+
+#eval negateOrIdentity true "yo"
diff --git a/nat.lean b/nat.lean
new file mode 100644
index 0000000..a373b06
--- /dev/null
+++ b/nat.lean
@@ -0,0 +1,76 @@
+-- This focuses more on the programming and type and programming
+-- side of lean than proving type.  All done here can be done in haskell.
+
+-- Pat = Pranshu's nat
+inductive Pat where
+  | zero : Pat
+  | succ (p : Pat) : Pat
+
+-- ntp stands for nat to pat
+def ntp (n : Nat) : Pat :=
+ match n with
+  | 0 => Pat.zero
+  | n'+1 => Pat.succ (ntp n')
+
+-- ptn = pat to nat
+def ptn (p : Pat) : Nat :=
+ match p with
+  | Pat.zero => 0
+  | Pat.succ n => 1 + ptn n
+
+-- True
+#eval let a := 10 ; (ptn (ntp a)) == a
+-- TODO prove properly using theorem or something
+
+-- in haskell this would be
+-- data Pat = Zero | Succ Pat
+
+def isZero (p : Pat) : Bool :=
+ match p with
+  | Pat.zero => true
+  | Pat.succ _ => false
+
+-- This is true
+#eval isZero Pat.zero
+
+------- Now I make basic functions -------
+
+def plus (l : Pat) (r : Pat) : Pat :=
+ match l with
+  | Pat.zero => r
+  | Pat.succ p => plus p (Pat.succ r)
+
+-- (Pat.succ Pat.zero)
+#eval plus Pat.zero (Pat.succ Pat.zero)
+
+-- (Pat.succ Pat.zero)
+#eval plus (Pat.succ Pat.zero) Pat.zero
+
+-- (Pat.succ (Pat.succ Pat.zero))
+#eval plus (Pat.succ Pat.zero) (Pat.succ Pat.zero)
+
+-- Pred is like `- 1`
+def pred (p : Pat) : Pat :=
+  match p with
+  | Pat.zero => Pat.zero
+  | Pat.succ k => k
+
+def sub (l : Pat) (r : Pat) : Pat :=
+ match r with
+  | Pat.zero => l
+  | Pat.succ p => pred (sub l p)
+
+def greater_than (p : Pat) (k : Pat) : Bool :=
+ match sub p k with
+   | Pat.zero => false
+   | _ => true
+
+-- False
+#eval greater_than (ntp 2) (ntp 3)
+
+-- -- ERROR 'failed to prove termination'
+-- def div (n : Pat) (k : Pat) : Pat :=
+--   if greater_than k n 
+--     then Pat.zero
+--   else Pat.succ (div (sub n k) k)
+-- termination_by?