-- 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"