## Idris syntax

 Idris $\blacktriangleright$ Idris syntax $\blacktriangleright$ ...

### Note

I'll try to take all the primitive notions and write down one example with them, respectively.

This list largely overlaps with Haskell.

##### Defining types
data Beagle	 = Bigtime | Burger | Bouncer | Baggy | Bankjob | Bugle | Babyface
data Kid   	 = Tick | Trick | Track
data Parent 	 = Donald | Dasy
data Grandparent = Dagobert

data Singleton   = Point
##### Prelude types
my_number : Int
my_number = 7
my_string : String
my_string = "a string"
my_char : Char
my_char = 'a'
my_bool : Bool
my_bool = False
##### Defining functions, explicitly
favorite_parent : Kid -> Parent
favorite_parent Trick = Dasy
favorite_parent k     = Donald -- k is any term of the Kid type

toPoint : Int -> Singleton
toPoint n = Point

toPointLambda : Int -> Singleton
toPointLambda = \n => Point

kid_identity : Kid -> Kid
identity k = k
##### Defining types 2, inductively by defining functions
data Nat_    = Z_ | S_ Nat_
-- Z_ : Nat_
-- S_ : Nat_ -> Nat_

data List_ a = End_ | Cons_ a (List_ a) -- here 'a' may be any type
-- List_ : Type -> Type
-- End_ : List_ a -- '[]' is the empty list
-- Cons_ : a -> List_ a -> List_ a -- '::' is usually used for Cons_
##### Defining functions, patter maching
plus : Nat_ -> Nat_ -> Nat_
plus Z_     y = y
plus (S_ k) y = S_ (plus k y) -- uses 'plus' again
##### Defining functions, dependent type
mkSingle : (x : Bool) -> natOrList x
mkSingle True = 0
mkSingle False = []

natOrList : Bool -> Type
natOrList True = Nat
natOrList False = List Nat
todo: check this
identity : (t : Type) -> t -> t
identity t = \x => x
##### Prelude functions
todo:
(==) : Eq ty => ty -> ty -> Bool
(*)  : Num ty => ty -> ty -> ty
(+)  : Num ty => ty -> ty -> ty
##### type, where
data Vect : Nat -> Type -> Type where
Nil  : Vect Z a
(::) : a -> Vect k a -> Vect (S k) a
##### functions, where
reverse : List a -> List a
reverse xs = revAcc [] xs where
revAcc : List a -> List a -> List a -- Indentation is significant here
revAcc acc [] = acc
revAcc acc (x :: xs) = revAcc (x :: acc) xs
##### case
case_fun : Int -> Int
case_fun x = case isLT of
Yes => x + 100
No  => x + 10
where
data MyLT = Yes | No
isLT : MyLT
isLT = if x < 20 then Yes else No
##### if
AorB : Bool -> String
AorB b = if b then "A" else "B" -- if-construction
##### For infix definitions

Here one may use those symbols in combinations

-- :+-*\/=.?|&><!@\$%^~#

except to form those predefined ones

-- : => -> <- = ?= | ** ==> \ % ~ ? !