Skip to content

Instantly share code, notes, and snippets.

@hamishdickson
Created March 4, 2017 13:49
Show Gist options
  • Save hamishdickson/5441a94014c9b91ae7ab3172b42a0d66 to your computer and use it in GitHub Desktop.
Save hamishdickson/5441a94014c9b91ae7ab3172b42a0d66 to your computer and use it in GitHub Desktop.
import Data.Vect
insert : Ord elem => (x : elem) -> (xsSorted : Vect k elem) -> Vect (S k) elem
insert x [] = [x]
insert x (y :: xs) = case x < y of
False => y :: insert x xs
True => x :: y :: xs
insSort : Ord elem => Vect n elem -> Vect n elem
insSort [] = []
insSort (x :: xs) = let xsSorted = insSort xs in
insert x xsSorted
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment