// Surface notation lowers to the same explicit contracts and primitive calls.
#generate #array:
  element #u64;
  length 4;
  name Array4;

#fn widen {
  #params = { index = #usize; };
  #returns = ();
  #requires:
    [#usize; index < 2];
  #ensures:
    [#usize; index < 4];
  #body:
    #return ();
}

#fn main {
  #params = {};
  #returns = #u64;
  #body:
    #let values Array4 (#array-of 10 42 30 40);
    #let index #usize 1;
    #return (#if-valid [#usize; index < 2]
      (#block
        (widen { index = index; })
        (Array4::get { values = (#borrow values); index = index; }))
      0u64);
}