quicksort ready for demo

This commit is contained in:
sebastianselander 2023-05-25 11:23:30 +02:00
parent 41934e2011
commit 5eed5fbcd1

View file

@ -23,6 +23,110 @@ filter p xs = case xs of
True => Cons x (filter p xs) True => Cons x (filter p xs)
False => filter p xs False => filter p xs
.++ : List a -> List a -> List a
.++ list1 list2 = case list1 of .++ list1 list2 = case list1 of
Nil => list2 Nil => list2
Cons x xs => Cons x (xs ++ list2) Cons x xs => Cons x (xs ++ list2)
printListH : List Int -> Unit
printListH xs = case xs of
Cons a as => flipConst (printInt a) (printListHH as)
Nil => Unit
printListHH : List Int -> Unit
printListHH xs = case xs of
Nil => Unit
Cons a as => flipConst (printChar ',') (flipConst (printInt a) (printListHH as))
printList : List Int -> Unit
printList xs = case Cons (printChar '[') (Cons (printListH xs) (Cons (printChar ']') Nil)) of
_ => Unit
flipConst x y = y
printInt : Int -> Unit
printInt xs = Unit
printChar : Char -> Unit
printChar = \x. Unit
data Unit where
Unit : Unit