(* Generated by coq-of-rust *)
Require Import CoqOfRust.CoqOfRust.

Module intrinsics.
  Module simd.
    Parameter simd_insert : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_insert : M.IsFunction "core::intrinsics::simd::simd_insert" simd_insert.
    
    Parameter simd_extract : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_extract : M.IsFunction "core::intrinsics::simd::simd_extract" simd_extract.
    
    Parameter simd_add : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_add : M.IsFunction "core::intrinsics::simd::simd_add" simd_add.
    
    Parameter simd_sub : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_sub : M.IsFunction "core::intrinsics::simd::simd_sub" simd_sub.
    
    Parameter simd_mul : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_mul : M.IsFunction "core::intrinsics::simd::simd_mul" simd_mul.
    
    Parameter simd_div : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_div : M.IsFunction "core::intrinsics::simd::simd_div" simd_div.
    
    Parameter simd_rem : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_rem : M.IsFunction "core::intrinsics::simd::simd_rem" simd_rem.
    
    Parameter simd_shl : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_shl : M.IsFunction "core::intrinsics::simd::simd_shl" simd_shl.
    
    Parameter simd_shr : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_shr : M.IsFunction "core::intrinsics::simd::simd_shr" simd_shr.
    
    Parameter simd_and : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_and : M.IsFunction "core::intrinsics::simd::simd_and" simd_and.
    
    Parameter simd_or : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_or : M.IsFunction "core::intrinsics::simd::simd_or" simd_or.
    
    Parameter simd_xor : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_xor : M.IsFunction "core::intrinsics::simd::simd_xor" simd_xor.
    
    Parameter simd_cast : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_cast : M.IsFunction "core::intrinsics::simd::simd_cast" simd_cast.
    
    Parameter simd_as : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_as : M.IsFunction "core::intrinsics::simd::simd_as" simd_as.
    
    Parameter simd_neg : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_neg : M.IsFunction "core::intrinsics::simd::simd_neg" simd_neg.
    
    Parameter simd_fabs : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_fabs : M.IsFunction "core::intrinsics::simd::simd_fabs" simd_fabs.
    
    Parameter simd_fmin : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_fmin : M.IsFunction "core::intrinsics::simd::simd_fmin" simd_fmin.
    
    Parameter simd_fmax : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_fmax : M.IsFunction "core::intrinsics::simd::simd_fmax" simd_fmax.
    
    Parameter simd_eq : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_eq : M.IsFunction "core::intrinsics::simd::simd_eq" simd_eq.
    
    Parameter simd_ne : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_ne : M.IsFunction "core::intrinsics::simd::simd_ne" simd_ne.
    
    Parameter simd_lt : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_lt : M.IsFunction "core::intrinsics::simd::simd_lt" simd_lt.
    
    Parameter simd_le : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_le : M.IsFunction "core::intrinsics::simd::simd_le" simd_le.
    
    Parameter simd_gt : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_gt : M.IsFunction "core::intrinsics::simd::simd_gt" simd_gt.
    
    Parameter simd_ge : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_ge : M.IsFunction "core::intrinsics::simd::simd_ge" simd_ge.
    
    Parameter simd_shuffle : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_shuffle : M.IsFunction "core::intrinsics::simd::simd_shuffle" simd_shuffle.
    
    Parameter simd_gather : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_gather : M.IsFunction "core::intrinsics::simd::simd_gather" simd_gather.
    
    Parameter simd_scatter : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_scatter : M.IsFunction "core::intrinsics::simd::simd_scatter" simd_scatter.
    
    Parameter simd_masked_load : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_masked_load :
      M.IsFunction "core::intrinsics::simd::simd_masked_load" simd_masked_load.
    
    Parameter simd_masked_store : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_masked_store :
      M.IsFunction "core::intrinsics::simd::simd_masked_store" simd_masked_store.
    
    Parameter simd_saturating_add : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_saturating_add :
      M.IsFunction "core::intrinsics::simd::simd_saturating_add" simd_saturating_add.
    
    Parameter simd_saturating_sub : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_saturating_sub :
      M.IsFunction "core::intrinsics::simd::simd_saturating_sub" simd_saturating_sub.
    
    Parameter simd_reduce_add_ordered : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_reduce_add_ordered :
      M.IsFunction "core::intrinsics::simd::simd_reduce_add_ordered" simd_reduce_add_ordered.
    
    Parameter simd_reduce_add_unordered : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_reduce_add_unordered :
      M.IsFunction "core::intrinsics::simd::simd_reduce_add_unordered" simd_reduce_add_unordered.
    
    Parameter simd_reduce_mul_ordered : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_reduce_mul_ordered :
      M.IsFunction "core::intrinsics::simd::simd_reduce_mul_ordered" simd_reduce_mul_ordered.
    
    Parameter simd_reduce_mul_unordered : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_reduce_mul_unordered :
      M.IsFunction "core::intrinsics::simd::simd_reduce_mul_unordered" simd_reduce_mul_unordered.
    
    Parameter simd_reduce_all : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_reduce_all :
      M.IsFunction "core::intrinsics::simd::simd_reduce_all" simd_reduce_all.
    
    Parameter simd_reduce_any : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_reduce_any :
      M.IsFunction "core::intrinsics::simd::simd_reduce_any" simd_reduce_any.
    
    Parameter simd_reduce_max : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_reduce_max :
      M.IsFunction "core::intrinsics::simd::simd_reduce_max" simd_reduce_max.
    
    Parameter simd_reduce_min : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_reduce_min :
      M.IsFunction "core::intrinsics::simd::simd_reduce_min" simd_reduce_min.
    
    Parameter simd_reduce_and : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_reduce_and :
      M.IsFunction "core::intrinsics::simd::simd_reduce_and" simd_reduce_and.
    
    Parameter simd_reduce_or : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_reduce_or :
      M.IsFunction "core::intrinsics::simd::simd_reduce_or" simd_reduce_or.
    
    Parameter simd_reduce_xor : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_reduce_xor :
      M.IsFunction "core::intrinsics::simd::simd_reduce_xor" simd_reduce_xor.
    
    Parameter simd_bitmask : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_bitmask : M.IsFunction "core::intrinsics::simd::simd_bitmask" simd_bitmask.
    
    Parameter simd_select : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_select : M.IsFunction "core::intrinsics::simd::simd_select" simd_select.
    
    Parameter simd_select_bitmask : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_select_bitmask :
      M.IsFunction "core::intrinsics::simd::simd_select_bitmask" simd_select_bitmask.
    
    Parameter simd_arith_offset : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_arith_offset :
      M.IsFunction "core::intrinsics::simd::simd_arith_offset" simd_arith_offset.
    
    Parameter simd_cast_ptr : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_cast_ptr :
      M.IsFunction "core::intrinsics::simd::simd_cast_ptr" simd_cast_ptr.
    
    Parameter simd_expose_provenance : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_expose_provenance :
      M.IsFunction "core::intrinsics::simd::simd_expose_provenance" simd_expose_provenance.
    
    Parameter simd_with_exposed_provenance : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_with_exposed_provenance :
      M.IsFunction
        "core::intrinsics::simd::simd_with_exposed_provenance"
        simd_with_exposed_provenance.
    
    Parameter simd_bswap : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_bswap : M.IsFunction "core::intrinsics::simd::simd_bswap" simd_bswap.
    
    Parameter simd_bitreverse : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_bitreverse :
      M.IsFunction "core::intrinsics::simd::simd_bitreverse" simd_bitreverse.
    
    Parameter simd_ctlz : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_ctlz : M.IsFunction "core::intrinsics::simd::simd_ctlz" simd_ctlz.
    
    Parameter simd_ctpop : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_ctpop : M.IsFunction "core::intrinsics::simd::simd_ctpop" simd_ctpop.
    
    Parameter simd_cttz : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_cttz : M.IsFunction "core::intrinsics::simd::simd_cttz" simd_cttz.
    
    Parameter simd_ceil : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_ceil : M.IsFunction "core::intrinsics::simd::simd_ceil" simd_ceil.
    
    Parameter simd_floor : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_floor : M.IsFunction "core::intrinsics::simd::simd_floor" simd_floor.
    
    Parameter simd_round : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_round : M.IsFunction "core::intrinsics::simd::simd_round" simd_round.
    
    Parameter simd_trunc : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_trunc : M.IsFunction "core::intrinsics::simd::simd_trunc" simd_trunc.
    
    Parameter simd_fsqrt : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_fsqrt : M.IsFunction "core::intrinsics::simd::simd_fsqrt" simd_fsqrt.
    
    Parameter simd_fma : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_fma : M.IsFunction "core::intrinsics::simd::simd_fma" simd_fma.
    
    Parameter simd_fsin : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_fsin : M.IsFunction "core::intrinsics::simd::simd_fsin" simd_fsin.
    
    Parameter simd_fcos : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_fcos : M.IsFunction "core::intrinsics::simd::simd_fcos" simd_fcos.
    
    Parameter simd_fexp : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_fexp : M.IsFunction "core::intrinsics::simd::simd_fexp" simd_fexp.
    
    Parameter simd_fexp2 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_fexp2 : M.IsFunction "core::intrinsics::simd::simd_fexp2" simd_fexp2.
    
    Parameter simd_flog10 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_flog10 : M.IsFunction "core::intrinsics::simd::simd_flog10" simd_flog10.
    
    Parameter simd_flog2 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_flog2 : M.IsFunction "core::intrinsics::simd::simd_flog2" simd_flog2.
    
    Parameter simd_flog : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Function_simd_flog : M.IsFunction "core::intrinsics::simd::simd_flog" simd_flog.
  End simd.
End intrinsics.
