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

Module intrinsics.
  Module mir.
    (*
    Enum BasicBlock
    {
      const_params := [];
      ty_params := [];
      variants :=
        [
          {
            name := "Normal";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "Cleanup";
            item := StructTuple [];
            discriminant := None;
          }
        ];
    }
    *)
    
    (*
    Enum UnwindTerminateReason
    {
      const_params := [];
      ty_params := [];
      variants :=
        [
          {
            name := "Abi";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "InCleanup";
            item := StructTuple [];
            discriminant := None;
          }
        ];
    }
    *)
    
    (* StructTuple
      {
        name := "UnwindActionArg";
        const_params := [];
        ty_params := [];
        fields := [];
      } *)
    
    (*         pub fn $($sig)* { panic!() } *)
    Definition value_UnwindContinue (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (M.never_to_any (|
            M.call_closure (|
              M.get_function (| "core::intrinsics::mir::UnwindContinue.panic_cold_explicit", [] |),
              []
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_value_UnwindContinue :
      M.IsFunction "core::intrinsics::mir::UnwindContinue" value_UnwindContinue.
    
    (*         pub fn $($sig)* { panic!() } *)
    Definition value_UnwindUnreachable (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (M.never_to_any (|
            M.call_closure (|
              M.get_function (|
                "core::intrinsics::mir::UnwindUnreachable.panic_cold_explicit",
                []
              |),
              []
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_value_UnwindUnreachable :
      M.IsFunction "core::intrinsics::mir::UnwindUnreachable" value_UnwindUnreachable.
    
    (*         pub fn $($sig)* { panic!() } *)
    Definition value_UnwindTerminate (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ reason ] =>
        ltac:(M.monadic
          (let reason := M.alloc (| reason |) in
          M.never_to_any (|
            M.call_closure (|
              M.get_function (| "core::intrinsics::mir::UnwindTerminate.panic_cold_explicit", [] |),
              []
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_value_UnwindTerminate :
      M.IsFunction "core::intrinsics::mir::UnwindTerminate" value_UnwindTerminate.
    
    (*         pub fn $($sig)* { panic!() } *)
    Definition value_UnwindCleanup (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ goto ] =>
        ltac:(M.monadic
          (let goto := M.alloc (| goto |) in
          M.never_to_any (|
            M.call_closure (|
              M.get_function (| "core::intrinsics::mir::UnwindCleanup.panic_cold_explicit", [] |),
              []
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_value_UnwindCleanup :
      M.IsFunction "core::intrinsics::mir::UnwindCleanup" value_UnwindCleanup.
    
    (* StructTuple
      {
        name := "ReturnToArg";
        const_params := [];
        ty_params := [];
        fields := [];
      } *)
    
    (*         pub fn $($sig)* { panic!() } *)
    Definition value_ReturnTo (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ goto ] =>
        ltac:(M.monadic
          (let goto := M.alloc (| goto |) in
          M.never_to_any (|
            M.call_closure (|
              M.get_function (| "core::intrinsics::mir::ReturnTo.panic_cold_explicit", [] |),
              []
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_value_ReturnTo : M.IsFunction "core::intrinsics::mir::ReturnTo" value_ReturnTo.
    
    (*         pub fn $($sig)* { panic!() } *)
    Definition value_Return (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (M.never_to_any (|
            M.call_closure (|
              M.get_function (| "core::intrinsics::mir::Return.panic_cold_explicit", [] |),
              []
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_value_Return : M.IsFunction "core::intrinsics::mir::Return" value_Return.
    
    (*         pub fn $($sig)* { panic!() } *)
    Definition value_Goto (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ destination ] =>
        ltac:(M.monadic
          (let destination := M.alloc (| destination |) in
          M.never_to_any (|
            M.call_closure (|
              M.get_function (| "core::intrinsics::mir::Goto.panic_cold_explicit", [] |),
              []
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_value_Goto : M.IsFunction "core::intrinsics::mir::Goto" value_Goto.
    
    (*         pub fn $($sig)* { panic!() } *)
    Definition value_Unreachable (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (M.never_to_any (|
            M.call_closure (|
              M.get_function (| "core::intrinsics::mir::Unreachable.panic_cold_explicit", [] |),
              []
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_value_Unreachable :
      M.IsFunction "core::intrinsics::mir::Unreachable" value_Unreachable.
    
    (*         pub fn $($sig)* { panic!() } *)
    Definition value_Drop (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ place; goto; unwind_action ] =>
        ltac:(M.monadic
          (let place := M.alloc (| place |) in
          let goto := M.alloc (| goto |) in
          let unwind_action := M.alloc (| unwind_action |) in
          M.never_to_any (|
            M.call_closure (|
              M.get_function (| "core::intrinsics::mir::Drop.panic_cold_explicit", [] |),
              []
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_value_Drop : M.IsFunction "core::intrinsics::mir::Drop" value_Drop.
    
    (*         pub fn $($sig)* { panic!() } *)
    Definition value_Call (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ call; goto; unwind_action ] =>
        ltac:(M.monadic
          (let call := M.alloc (| call |) in
          let goto := M.alloc (| goto |) in
          let unwind_action := M.alloc (| unwind_action |) in
          M.never_to_any (|
            M.call_closure (|
              M.get_function (| "core::intrinsics::mir::Call.panic_cold_explicit", [] |),
              []
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_value_Call : M.IsFunction "core::intrinsics::mir::Call" value_Call.
    
    (*         pub fn $($sig)* { panic!() } *)
    Definition value_TailCall (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ call ] =>
        ltac:(M.monadic
          (let call := M.alloc (| call |) in
          M.never_to_any (|
            M.call_closure (|
              M.get_function (| "core::intrinsics::mir::TailCall.panic_cold_explicit", [] |),
              []
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_value_TailCall : M.IsFunction "core::intrinsics::mir::TailCall" value_TailCall.
    
    (*         pub fn $($sig)* { panic!() } *)
    Definition value_UnwindResume (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (M.never_to_any (|
            M.call_closure (|
              M.get_function (| "core::intrinsics::mir::UnwindResume.panic_cold_explicit", [] |),
              []
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_value_UnwindResume :
      M.IsFunction "core::intrinsics::mir::UnwindResume" value_UnwindResume.
    
    (*         pub fn $($sig)* { panic!() } *)
    Definition value_StorageLive (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ local ] =>
        ltac:(M.monadic
          (let local := M.alloc (| local |) in
          M.never_to_any (|
            M.call_closure (|
              M.get_function (| "core::intrinsics::mir::StorageLive.panic_cold_explicit", [] |),
              []
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_value_StorageLive :
      M.IsFunction "core::intrinsics::mir::StorageLive" value_StorageLive.
    
    (*         pub fn $($sig)* { panic!() } *)
    Definition value_StorageDead (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ local ] =>
        ltac:(M.monadic
          (let local := M.alloc (| local |) in
          M.never_to_any (|
            M.call_closure (|
              M.get_function (| "core::intrinsics::mir::StorageDead.panic_cold_explicit", [] |),
              []
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_value_StorageDead :
      M.IsFunction "core::intrinsics::mir::StorageDead" value_StorageDead.
    
    (*         pub fn $($sig)* { panic!() } *)
    Definition value_Assume (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ operand ] =>
        ltac:(M.monadic
          (let operand := M.alloc (| operand |) in
          M.never_to_any (|
            M.call_closure (|
              M.get_function (| "core::intrinsics::mir::Assume.panic_cold_explicit", [] |),
              []
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_value_Assume : M.IsFunction "core::intrinsics::mir::Assume" value_Assume.
    
    (*         pub fn $($sig)* { panic!() } *)
    Definition value_Deinit (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ place ] =>
        ltac:(M.monadic
          (let place := M.alloc (| place |) in
          M.never_to_any (|
            M.call_closure (|
              M.get_function (| "core::intrinsics::mir::Deinit.panic_cold_explicit", [] |),
              []
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_value_Deinit : M.IsFunction "core::intrinsics::mir::Deinit" value_Deinit.
    
    (*         pub fn $($sig)* { panic!() } *)
    Definition value_Checked (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ binop ] =>
        ltac:(M.monadic
          (let binop := M.alloc (| binop |) in
          M.never_to_any (|
            M.call_closure (|
              M.get_function (| "core::intrinsics::mir::Checked.panic_cold_explicit", [] |),
              []
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_value_Checked : M.IsFunction "core::intrinsics::mir::Checked" value_Checked.
    
    (*         pub fn $($sig)* { panic!() } *)
    Definition value_Len (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ place ] =>
        ltac:(M.monadic
          (let place := M.alloc (| place |) in
          M.never_to_any (|
            M.call_closure (|
              M.get_function (| "core::intrinsics::mir::Len.panic_cold_explicit", [] |),
              []
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_value_Len : M.IsFunction "core::intrinsics::mir::Len" value_Len.
    
    (*         pub fn $($sig)* { panic!() } *)
    Definition value_PtrMetadata (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ P ], [ place ] =>
        ltac:(M.monadic
          (let place := M.alloc (| place |) in
          M.never_to_any (|
            M.call_closure (|
              M.get_function (| "core::intrinsics::mir::PtrMetadata.panic_cold_explicit", [] |),
              []
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_value_PtrMetadata :
      M.IsFunction "core::intrinsics::mir::PtrMetadata" value_PtrMetadata.
    
    (*         pub fn $($sig)* { panic!() } *)
    Definition value_CopyForDeref (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ place ] =>
        ltac:(M.monadic
          (let place := M.alloc (| place |) in
          M.never_to_any (|
            M.call_closure (|
              M.get_function (| "core::intrinsics::mir::CopyForDeref.panic_cold_explicit", [] |),
              []
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_value_CopyForDeref :
      M.IsFunction "core::intrinsics::mir::CopyForDeref" value_CopyForDeref.
    
    (*         pub fn $($sig)* { panic!() } *)
    Definition value_Retag (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ place ] =>
        ltac:(M.monadic
          (let place := M.alloc (| place |) in
          M.never_to_any (|
            M.call_closure (|
              M.get_function (| "core::intrinsics::mir::Retag.panic_cold_explicit", [] |),
              []
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_value_Retag : M.IsFunction "core::intrinsics::mir::Retag" value_Retag.
    
    (*         pub fn $($sig)* { panic!() } *)
    Definition value_Move (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ place ] =>
        ltac:(M.monadic
          (let place := M.alloc (| place |) in
          M.never_to_any (|
            M.call_closure (|
              M.get_function (| "core::intrinsics::mir::Move.panic_cold_explicit", [] |),
              []
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_value_Move : M.IsFunction "core::intrinsics::mir::Move" value_Move.
    
    (*         pub fn $($sig)* { panic!() } *)
    Definition value_Static (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ s ] =>
        ltac:(M.monadic
          (let s := M.alloc (| s |) in
          M.never_to_any (|
            M.call_closure (|
              M.get_function (| "core::intrinsics::mir::Static.panic_cold_explicit", [] |),
              []
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_value_Static : M.IsFunction "core::intrinsics::mir::Static" value_Static.
    
    (*         pub fn $($sig)* { panic!() } *)
    Definition value_StaticMut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ s ] =>
        ltac:(M.monadic
          (let s := M.alloc (| s |) in
          M.never_to_any (|
            M.call_closure (|
              M.get_function (| "core::intrinsics::mir::StaticMut.panic_cold_explicit", [] |),
              []
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_value_StaticMut :
      M.IsFunction "core::intrinsics::mir::StaticMut" value_StaticMut.
    
    (*         pub fn $($sig)* { panic!() } *)
    Definition value_Discriminant (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ place ] =>
        ltac:(M.monadic
          (let place := M.alloc (| place |) in
          M.never_to_any (|
            M.call_closure (|
              M.get_function (| "core::intrinsics::mir::Discriminant.panic_cold_explicit", [] |),
              []
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_value_Discriminant :
      M.IsFunction "core::intrinsics::mir::Discriminant" value_Discriminant.
    
    (*         pub fn $($sig)* { panic!() } *)
    Definition value_SetDiscriminant (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ place; index ] =>
        ltac:(M.monadic
          (let place := M.alloc (| place |) in
          let index := M.alloc (| index |) in
          M.never_to_any (|
            M.call_closure (|
              M.get_function (| "core::intrinsics::mir::SetDiscriminant.panic_cold_explicit", [] |),
              []
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_value_SetDiscriminant :
      M.IsFunction "core::intrinsics::mir::SetDiscriminant" value_SetDiscriminant.
    
    (*         pub fn $($sig)* { panic!() } *)
    Definition value_Offset (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T; U ], [ ptr; count ] =>
        ltac:(M.monadic
          (let ptr := M.alloc (| ptr |) in
          let count := M.alloc (| count |) in
          M.never_to_any (|
            M.call_closure (|
              M.get_function (| "core::intrinsics::mir::Offset.panic_cold_explicit", [] |),
              []
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_value_Offset : M.IsFunction "core::intrinsics::mir::Offset" value_Offset.
    
    (*         pub fn $($sig)* { panic!() } *)
    Definition value_Field (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ F ], [ place; field ] =>
        ltac:(M.monadic
          (let place := M.alloc (| place |) in
          let field := M.alloc (| field |) in
          M.never_to_any (|
            M.call_closure (|
              M.get_function (| "core::intrinsics::mir::Field.panic_cold_explicit", [] |),
              []
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_value_Field : M.IsFunction "core::intrinsics::mir::Field" value_Field.
    
    (*         pub fn $($sig)* { panic!() } *)
    Definition value_Variant (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ place; index ] =>
        ltac:(M.monadic
          (let place := M.alloc (| place |) in
          let index := M.alloc (| index |) in
          M.never_to_any (|
            M.call_closure (|
              M.get_function (| "core::intrinsics::mir::Variant.panic_cold_explicit", [] |),
              []
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_value_Variant : M.IsFunction "core::intrinsics::mir::Variant" value_Variant.
    
    (*         pub fn $($sig)* { panic!() } *)
    Definition value_CastTransmute (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T; U ], [ operand ] =>
        ltac:(M.monadic
          (let operand := M.alloc (| operand |) in
          M.never_to_any (|
            M.call_closure (|
              M.get_function (| "core::intrinsics::mir::CastTransmute.panic_cold_explicit", [] |),
              []
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_value_CastTransmute :
      M.IsFunction "core::intrinsics::mir::CastTransmute" value_CastTransmute.
    
    (*         pub fn $($sig)* { panic!() } *)
    Definition value_CastPtrToPtr (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T; U ], [ operand ] =>
        ltac:(M.monadic
          (let operand := M.alloc (| operand |) in
          M.never_to_any (|
            M.call_closure (|
              M.get_function (| "core::intrinsics::mir::CastPtrToPtr.panic_cold_explicit", [] |),
              []
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_value_CastPtrToPtr :
      M.IsFunction "core::intrinsics::mir::CastPtrToPtr" value_CastPtrToPtr.
    
    (*         pub fn $($sig)* { panic!() } *)
    Definition __internal_make_place (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ place ] =>
        ltac:(M.monadic
          (let place := M.alloc (| place |) in
          M.never_to_any (|
            M.call_closure (|
              M.get_function (|
                "core::intrinsics::mir::__internal_make_place.panic_cold_explicit",
                []
              |),
              []
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function___internal_make_place :
      M.IsFunction "core::intrinsics::mir::__internal_make_place" __internal_make_place.
    
    (*         pub fn $($sig)* { panic!() } *)
    Definition __debuginfo (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ name; s ] =>
        ltac:(M.monadic
          (let name := M.alloc (| name |) in
          let s := M.alloc (| s |) in
          M.never_to_any (|
            M.call_closure (|
              M.get_function (| "core::intrinsics::mir::__debuginfo.panic_cold_explicit", [] |),
              []
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function___debuginfo : M.IsFunction "core::intrinsics::mir::__debuginfo" __debuginfo.
  End mir.
End intrinsics.
