mstewartgallus

/// This type is only every inhabited when S is nominally equivalent to T
pub type Is <S, T> = Is_ <S, T>;

priv struct Is_ <S, T>;

// Construct a proof of the fact that a type is nominally equivalent
// to itself.
pub fn Is <T> () -> Is <T, T> { Is_ }

pub impl <S, T> Is_ <S, T> {

ctford

insert : Ord a => a -> Vect n a -> Vect (1 + n) a
insert x [] = [x]
insert x (y::ys) with (x <= y)
  | True = x::y::ys
  | False = y::insert x ys 

isort : Ord a => Vect n a -> Vect n a
isort [] = []
isort (x::xs) = insert x (isort xs)