(*
%use "Sundry/append.fsh" ;;
*)

(*
append : [a] -> [a] -> [a]

actually does joining of blocks 
*)


let append x y = 
  check (preddim #x #= (preddim #y)) (
  let m = lendim #x
  and n = lendim #y in  
  new #z = succdim (m+n) (preddim #x) 
  in 
  for i< m do
    sub(z,i) := sub(x,i)
  done ;
  for i<n do
    sub(z,m+i) := sub(y,i)
  done
  return z )
;;