churf/sample-programs/insertion-sort.chrf

23 lines
573 B
Text

data List (a) where
Nil : List (a)
Cons : a -> List (a) -> List (a)
insert : Int -> List (Int) -> List (Int)
insert x xs = case xs of
Cons z zs => case (lt x z) of
True => Cons x (Cons z zs)
False => Cons z (insert x zs)
Nil => Cons x Nil
insertionSort : List (Int) -> List (Int)
insertionSort xs = case xs of
Cons y ys => case ys of
_ => insert y (insertionSort ys)
Nil => xs
Nil => Nil
main = head (insertionSort (Cons 5 (Cons 4 (Cons 3 (Cons 2 (Cons 1 Nil))))))
head xs = case xs of
Cons x _ => x