datatype t = datatype Basis.list val show (a ::: Type) (_ : show a) = let fun show' (ls : list a) = case ls of [] => "[]" | x :: ls => show x ^ " :: " ^ show' ls in mkShow show' end val rev (a ::: Type) = let fun rev' acc (ls : list a) = case ls of [] => acc | x :: ls => rev' (x :: acc) ls in rev' [] end fun mp (a ::: Type) (b ::: Type) f = let fun mp' acc ls = case ls of [] => rev acc | x :: ls => mp' (f x :: acc) ls in mp' [] end fun mapX (a ::: Type) (ctx ::: {Unit}) f = let fun mapX' ls = case ls of [] => | x :: ls => {f x}{mapX' ls} in mapX' end fun mapM (m ::: (Type -> Type)) (_ : monad m) (a ::: Type) (b ::: Type) f = let fun mapM' acc ls = case ls of [] => acc | x :: ls => mapM' (x' <- f x; ls' <- acc; return (x' :: ls')) ls in mapM' (return []) end