32 lines
832 B
Text
32 lines
832 B
Text
|
||
|
||
-- 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"
|