type byte = u8; type uint32 = u32; type UInt32Array = uint32[N]; type matrix = field[R][C]; def fill(field v) -> matrix { return [[v; C]; R]; } def main(uint32 a, uint32 b) -> (UInt32Array<2>, matrix<2, 4>) { UInt32Array<2> res = [a, b]; matrix<2, 4> m = fill(1); return (res, m); }