val transpose4x4_0: #t:v_inttype -> vec_t4 t -> vec_t4 t
let transpose4x4_0 #t (v0,v1,v2,v3) =
  let v0' = vec_interleave_low v0 v1 in
  let v1' = vec_interleave_high v0 v1 in
  let v2' = vec_interleave_low v2 v3 in
  let v3' = vec_interleave_high v2 v3 in

  let v0'' = vec_interleave_low_n 2 v0' v2' in
  let v1'' = vec_interleave_high_n 2 v0' v2' in
  let v2'' = vec_interleave_low_n 2 v1' v3' in
  let v3'' = vec_interleave_high_n 2 v1' v3' in
  (v0'',v2'',v1'',v3'')
val transpose4x4_0: #t:v_inttype -> vec_t4 t -> vec_t4 t
let transpose4x4_0 #t (v0, v1, v2, v3) =
let v0' = vec_interleave_low v0 v1 in
let v1' = vec_interleave_high v0 v1 in
let v2' = vec_interleave_low v2 v3 in
let v3' = vec_interleave_high v2 v3 in
let v0'' = vec_interleave_low_n 2 v0' v2' in
let v1'' = vec_interleave_high_n 2 v0' v2' in
let v2'' = vec_interleave_low_n 2 v1' v3' in
let v3'' = vec_interleave_high_n 2 v1' v3' in
(v0'', v2'', v1'', v3'')
Lib.IntVector.Transpose.fst.checked
prims.fst.checked Lib.LoopCombinators.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Math.Lemmas.fst.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Lib.IntVector.Transpose.fst
Lib.IntVector.v_inttype Lib.IntVector.Transpose.vec_t4 Lib.IntVector.vec_t FStar.Pervasives.Native.Mktuple4 Lib.IntVector.vec_interleave_high_n Lib.IntVector.vec_interleave_low_n Lib.IntVector.vec_interleave_high Lib.IntVector.vec_interleave_low
module Lib.IntVector.Transpose

module Loops = Lib.LoopCombinators


#set-options "--z3rlimit 50 --fuel 0 --ifuel 0"

///
///  transpose4x4
///

inline_for_extraction
val transpose4x4_0: #t:v_inttype -> vec_t4 t -> vec_t4 t
_: Lib.IntVector.Transpose.vec_t4 t -> Lib.IntVector.Transpose.vec_t4 t