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

Module mem.
  (*
  pub const fn forget<T>(t: T) {
      let _ = ManuallyDrop::new(t);
  }
  *)
  Definition forget (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ t ] =>
      ltac:(M.monadic
        (let t := M.alloc (| t |) in
        M.read (|
          M.match_operator (|
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::mem::manually_drop::ManuallyDrop") [] [ T ],
                  "new",
                  []
                |),
                [ M.read (| t |) ]
              |)
            |),
            [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_forget : M.IsFunction "core::mem::forget" forget.
  
  (*
  pub fn forget_unsized<T: ?Sized>(t: T) {
      intrinsics::forget(t)
  }
  *)
  Definition forget_unsized (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ t ] =>
      ltac:(M.monadic
        (let t := M.alloc (| t |) in
        M.call_closure (|
          M.get_function (| "core::intrinsics::forget", [ T ] |),
          [ M.read (| t |) ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_forget_unsized : M.IsFunction "core::mem::forget_unsized" forget_unsized.
  
  (*
  pub const fn size_of<T>() -> usize {
      intrinsics::size_of::<T>()
  }
  *)
  Definition size_of (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [] =>
      ltac:(M.monadic
        (M.call_closure (| M.get_function (| "core::intrinsics::size_of", [ T ] |), [] |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_size_of : M.IsFunction "core::mem::size_of" size_of.
  
  (*
  pub const fn size_of_val<T: ?Sized>(val: &T) -> usize {
      // SAFETY: `val` is a reference, so it's a valid raw pointer
      unsafe { intrinsics::size_of_val(val) }
  }
  *)
  Definition size_of_val (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ val ] =>
      ltac:(M.monadic
        (let val := M.alloc (| val |) in
        M.call_closure (|
          M.get_function (| "core::intrinsics::size_of_val", [ T ] |),
          [ M.read (| val |) ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_size_of_val : M.IsFunction "core::mem::size_of_val" size_of_val.
  
  (*
  pub const unsafe fn size_of_val_raw<T: ?Sized>(val: *const T) -> usize {
      // SAFETY: the caller must provide a valid raw pointer
      unsafe { intrinsics::size_of_val(val) }
  }
  *)
  Definition size_of_val_raw (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ val ] =>
      ltac:(M.monadic
        (let val := M.alloc (| val |) in
        M.call_closure (|
          M.get_function (| "core::intrinsics::size_of_val", [ T ] |),
          [ M.read (| val |) ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_size_of_val_raw : M.IsFunction "core::mem::size_of_val_raw" size_of_val_raw.
  
  (*
  pub fn min_align_of<T>() -> usize {
      intrinsics::min_align_of::<T>()
  }
  *)
  Definition min_align_of (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [] =>
      ltac:(M.monadic
        (M.call_closure (| M.get_function (| "core::intrinsics::min_align_of", [ T ] |), [] |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_min_align_of : M.IsFunction "core::mem::min_align_of" min_align_of.
  
  (*
  pub fn min_align_of_val<T: ?Sized>(val: &T) -> usize {
      // SAFETY: val is a reference, so it's a valid raw pointer
      unsafe { intrinsics::min_align_of_val(val) }
  }
  *)
  Definition min_align_of_val (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ val ] =>
      ltac:(M.monadic
        (let val := M.alloc (| val |) in
        M.call_closure (|
          M.get_function (| "core::intrinsics::min_align_of_val", [ T ] |),
          [ M.read (| val |) ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_min_align_of_val : M.IsFunction "core::mem::min_align_of_val" min_align_of_val.
  
  (*
  pub const fn align_of<T>() -> usize {
      intrinsics::min_align_of::<T>()
  }
  *)
  Definition align_of (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [] =>
      ltac:(M.monadic
        (M.call_closure (| M.get_function (| "core::intrinsics::min_align_of", [ T ] |), [] |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_align_of : M.IsFunction "core::mem::align_of" align_of.
  
  (*
  pub const fn align_of_val<T: ?Sized>(val: &T) -> usize {
      // SAFETY: val is a reference, so it's a valid raw pointer
      unsafe { intrinsics::min_align_of_val(val) }
  }
  *)
  Definition align_of_val (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ val ] =>
      ltac:(M.monadic
        (let val := M.alloc (| val |) in
        M.call_closure (|
          M.get_function (| "core::intrinsics::min_align_of_val", [ T ] |),
          [ M.read (| val |) ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_align_of_val : M.IsFunction "core::mem::align_of_val" align_of_val.
  
  (*
  pub const unsafe fn align_of_val_raw<T: ?Sized>(val: *const T) -> usize {
      // SAFETY: the caller must provide a valid raw pointer
      unsafe { intrinsics::min_align_of_val(val) }
  }
  *)
  Definition align_of_val_raw (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ val ] =>
      ltac:(M.monadic
        (let val := M.alloc (| val |) in
        M.call_closure (|
          M.get_function (| "core::intrinsics::min_align_of_val", [ T ] |),
          [ M.read (| val |) ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_align_of_val_raw : M.IsFunction "core::mem::align_of_val_raw" align_of_val_raw.
  
  (*
  pub const fn needs_drop<T: ?Sized>() -> bool {
      intrinsics::needs_drop::<T>()
  }
  *)
  Definition needs_drop (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [] =>
      ltac:(M.monadic
        (M.call_closure (| M.get_function (| "core::intrinsics::needs_drop", [ T ] |), [] |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_needs_drop : M.IsFunction "core::mem::needs_drop" needs_drop.
  
  (*
  pub const unsafe fn zeroed<T>() -> T {
      // SAFETY: the caller must guarantee that an all-zero value is valid for `T`.
      unsafe {
          intrinsics::assert_zero_valid::<T>();
          MaybeUninit::zeroed().assume_init()
      }
  }
  *)
  Definition zeroed (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [] =>
      ltac:(M.monadic
        (M.read (|
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_function (| "core::intrinsics::assert_zero_valid", [ T ] |),
                []
              |)
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ],
                "assume_init",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ],
                    "zeroed",
                    []
                  |),
                  []
                |)
              ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_zeroed : M.IsFunction "core::mem::zeroed" zeroed.
  
  (*
  pub unsafe fn uninitialized<T>() -> T {
      // SAFETY: the caller must guarantee that an uninitialized value is valid for `T`.
      unsafe {
          intrinsics::assert_mem_uninitialized_valid::<T>();
          let mut val = MaybeUninit::<T>::uninit();
  
          // Fill memory with 0x01, as an imperfect mitigation for old code that uses this function on
          // bool, nonnull, and noundef types. But don't do this if we actively want to detect UB.
          if !cfg!(any(miri, sanitize = "memory")) {
              val.as_mut_ptr().write_bytes(0x01, 1);
          }
  
          val.assume_init()
      }
  }
  *)
  Definition uninitialized (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [] =>
      ltac:(M.monadic
        (M.read (|
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_function (| "core::intrinsics::assert_mem_uninitialized_valid", [ T ] |),
                []
              |)
            |) in
          let~ val :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ],
                  "uninit",
                  []
                |),
                []
              |)
            |) in
          let~ _ :=
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.use (M.alloc (| UnOp.not (| Value.Bool false |) |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    let~ _ :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "*mut") [] [ T ],
                            "write_bytes",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ],
                                "as_mut_ptr",
                                []
                              |),
                              [ val ]
                            |);
                            Value.Integer IntegerKind.U8 1;
                            Value.Integer IntegerKind.Usize 1
                          ]
                        |)
                      |) in
                    M.alloc (| Value.Tuple [] |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
              ]
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ],
                "assume_init",
                []
              |),
              [ M.read (| val |) ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_uninitialized : M.IsFunction "core::mem::uninitialized" uninitialized.
  
  (*
  pub const fn swap<T>(x: &mut T, y: &mut T) {
      // SAFETY: `&mut` guarantees these are typed readable and writable
      // as well as non-overlapping.
      unsafe { intrinsics::typed_swap(x, y) }
  }
  *)
  Definition swap (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ x; y ] =>
      ltac:(M.monadic
        (let x := M.alloc (| x |) in
        let y := M.alloc (| y |) in
        M.call_closure (|
          M.get_function (| "core::intrinsics::typed_swap", [ T ] |),
          [ M.read (| x |); M.read (| y |) ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_swap : M.IsFunction "core::mem::swap" swap.
  
  (*
  pub fn take<T: Default>(dest: &mut T) -> T {
      replace(dest, T::default())
  }
  *)
  Definition take (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ dest ] =>
      ltac:(M.monadic
        (let dest := M.alloc (| dest |) in
        M.call_closure (|
          M.get_function (| "core::mem::replace", [ T ] |),
          [
            M.read (| dest |);
            M.call_closure (|
              M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
              []
            |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_take : M.IsFunction "core::mem::take" take.
  
  (*
  pub const fn replace<T>(dest: &mut T, src: T) -> T {
      // It may be tempting to use `swap` to avoid `unsafe` here. Don't!
      // The compiler optimizes the implementation below to two `memcpy`s
      // while `swap` would require at least three. See PR#83022 for details.
  
      // SAFETY: We read from `dest` but directly write `src` into it afterwards,
      // such that the old value is not duplicated. Nothing is dropped and
      // nothing here can panic.
      unsafe {
          let result = ptr::read(dest);
          ptr::write(dest, src);
          result
      }
  }
  *)
  Definition replace (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ dest; src ] =>
      ltac:(M.monadic
        (let dest := M.alloc (| dest |) in
        let src := M.alloc (| src |) in
        M.read (|
          let~ result :=
            M.alloc (|
              M.call_closure (|
                M.get_function (| "core::ptr::read", [ T ] |),
                [ M.read (| dest |) ]
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_function (| "core::ptr::write", [ T ] |),
                [ M.read (| dest |); M.read (| src |) ]
              |)
            |) in
          result
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_replace : M.IsFunction "core::mem::replace" replace.
  
  (* pub fn drop<T>(_x: T) {} *)
  Definition drop (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ _x ] =>
      ltac:(M.monadic
        (let _x := M.alloc (| _x |) in
        Value.Tuple []))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_drop : M.IsFunction "core::mem::drop" drop.
  
  (*
  pub const fn copy<T: Copy>(x: &T) -> T {
      *x
  }
  *)
  Definition copy (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ x ] =>
      ltac:(M.monadic
        (let x := M.alloc (| x |) in
        M.read (| M.read (| x |) |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_copy : M.IsFunction "core::mem::copy" copy.
  
  (*
  pub const unsafe fn transmute_copy<Src, Dst>(src: &Src) -> Dst {
      assert!(
          size_of::<Src>() >= size_of::<Dst>(),
          "cannot transmute_copy if Dst is larger than Src"
      );
  
      // If Dst has a higher alignment requirement, src might not be suitably aligned.
      if align_of::<Dst>() > align_of::<Src>() {
          // SAFETY: `src` is a reference which is guaranteed to be valid for reads.
          // The caller must guarantee that the actual transmutation is safe.
          unsafe { ptr::read_unaligned(src as *const Src as *const Dst) }
      } else {
          // SAFETY: `src` is a reference which is guaranteed to be valid for reads.
          // We just checked that `src as *const Dst` was properly aligned.
          // The caller must guarantee that the actual transmutation is safe.
          unsafe { ptr::read(src as *const Src as *const Dst) }
      }
  }
  *)
  Definition transmute_copy (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ Src; Dst ], [ src ] =>
      ltac:(M.monadic
        (let src := M.alloc (| src |) in
        M.read (|
          let~ _ :=
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          UnOp.not (|
                            BinOp.ge (|
                              M.call_closure (|
                                M.get_function (| "core::mem::size_of", [ Src ] |),
                                []
                              |),
                              M.call_closure (|
                                M.get_function (| "core::mem::size_of", [ Dst ] |),
                                []
                              |)
                            |)
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      M.never_to_any (|
                        M.call_closure (|
                          M.get_function (| "core::panicking::panic_fmt", [] |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::Arguments",
                                "new_const",
                                []
                              |),
                              [
                                M.alloc (|
                                  Value.Array
                                    [
                                      M.read (|
                                        Value.String
                                          "cannot transmute_copy if Dst is larger than Src"
                                      |)
                                    ]
                                |)
                              ]
                            |)
                          ]
                        |)
                      |)
                    |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
              ]
            |) in
          M.match_operator (|
            M.alloc (| Value.Tuple [] |),
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ :=
                    M.use
                      (M.alloc (|
                        BinOp.gt (|
                          M.call_closure (|
                            M.get_function (| "core::mem::align_of", [ Dst ] |),
                            []
                          |),
                          M.call_closure (|
                            M.get_function (| "core::mem::align_of", [ Src ] |),
                            []
                          |)
                        |)
                      |)) in
                  let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (| "core::ptr::read_unaligned", [ Dst ] |),
                      [ M.rust_cast (M.read (| M.use (M.alloc (| M.read (| src |) |)) |)) ]
                    |)
                  |)));
              fun γ =>
                ltac:(M.monadic
                  (M.alloc (|
                    M.call_closure (|
                      M.get_function (| "core::ptr::read", [ Dst ] |),
                      [ M.rust_cast (M.read (| M.use (M.alloc (| M.read (| src |) |)) |)) ]
                    |)
                  |)))
            ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_transmute_copy : M.IsFunction "core::mem::transmute_copy" transmute_copy.
  
  (* StructTuple
    {
      name := "Discriminant";
      const_params := [];
      ty_params := [ "T" ];
      fields := [ Ty.associated ];
    } *)
  
  Module Impl_core_marker_Copy_for_core_mem_Discriminant_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::mem::Discriminant") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::marker::Copy"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_for_core_mem_Discriminant_T.
  
  Module Impl_core_clone_Clone_for_core_mem_Discriminant_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::mem::Discriminant") [] [ T ].
    
    (*
        fn clone(&self) -> Self {
            *self
        }
    *)
    Definition clone (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (| M.read (| self |) |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::clone::Clone"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("clone", InstanceField.Method (clone T)) ].
  End Impl_core_clone_Clone_for_core_mem_Discriminant_T.
  
  Module Impl_core_cmp_PartialEq_for_core_mem_Discriminant_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::mem::Discriminant") [] [ T ].
    
    (*
        fn eq(&self, rhs: &Self) -> bool {
            self.0 == rhs.0
        }
    *)
    Definition eq (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::cmp::PartialEq",
              Ty.associated,
              [ Ty.associated ],
              "eq",
              []
            |),
            [
              M.SubPointer.get_struct_tuple_field (|
                M.read (| self |),
                "core::mem::Discriminant",
                0
              |);
              M.SubPointer.get_struct_tuple_field (|
                M.read (| rhs |),
                "core::mem::Discriminant",
                0
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::cmp::PartialEq"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("eq", InstanceField.Method (eq T)) ].
  End Impl_core_cmp_PartialEq_for_core_mem_Discriminant_T.
  
  Module Impl_core_cmp_Eq_for_core_mem_Discriminant_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::mem::Discriminant") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance "core::cmp::Eq" (Self T) (* Trait polymorphic types *) [] (* Instance *) [].
  End Impl_core_cmp_Eq_for_core_mem_Discriminant_T.
  
  Module Impl_core_hash_Hash_for_core_mem_Discriminant_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::mem::Discriminant") [] [ T ].
    
    (*
        fn hash<H: hash::Hasher>(&self, state: &mut H) {
            self.0.hash(state);
        }
    *)
    Definition hash (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [ H ], [ self; state ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let state := M.alloc (| state |) in
          M.read (|
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (| "core::hash::Hash", Ty.associated, [], "hash", [ H ] |),
                  [
                    M.SubPointer.get_struct_tuple_field (|
                      M.read (| self |),
                      "core::mem::Discriminant",
                      0
                    |);
                    M.read (| state |)
                  ]
                |)
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::hash::Hash"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("hash", InstanceField.Method (hash T)) ].
  End Impl_core_hash_Hash_for_core_mem_Discriminant_T.
  
  Module Impl_core_fmt_Debug_for_core_mem_Discriminant_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::mem::Discriminant") [] [ T ].
    
    (*
        fn fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result {
            fmt.debug_tuple("Discriminant").field(&self.0).finish()
        }
    *)
    Definition fmt (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self; fmt ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let fmt := M.alloc (| fmt |) in
          M.call_closure (|
            M.get_associated_function (| Ty.path "core::fmt::builders::DebugTuple", "finish", [] |),
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "core::fmt::builders::DebugTuple",
                  "field",
                  []
                |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "core::fmt::Formatter",
                        "debug_tuple",
                        []
                      |),
                      [ M.read (| fmt |); M.read (| Value.String "Discriminant" |) ]
                    |)
                  |);
                  M.SubPointer.get_struct_tuple_field (|
                    M.read (| self |),
                    "core::mem::Discriminant",
                    0
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::fmt::Debug"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method (fmt T)) ].
  End Impl_core_fmt_Debug_for_core_mem_Discriminant_T.
  
  (*
  pub const fn discriminant<T>(v: &T) -> Discriminant<T> {
      Discriminant(intrinsics::discriminant_value(v))
  }
  *)
  Definition discriminant (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ v ] =>
      ltac:(M.monadic
        (let v := M.alloc (| v |) in
        Value.StructTuple
          "core::mem::Discriminant"
          [
            M.call_closure (|
              M.get_function (| "core::intrinsics::discriminant_value", [ T ] |),
              [ M.read (| v |) ]
            |)
          ]))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_discriminant : M.IsFunction "core::mem::discriminant" discriminant.
  
  (*
  pub const fn variant_count<T>() -> usize {
      intrinsics::variant_count::<T>()
  }
  *)
  Definition variant_count (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [] =>
      ltac:(M.monadic
        (M.call_closure (| M.get_function (| "core::intrinsics::variant_count", [ T ] |), [] |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_variant_count : M.IsFunction "core::mem::variant_count" variant_count.
  
  (* Trait *)
  (* Empty module 'SizedTypeProperties' *)
  
  Module Impl_core_mem_SizedTypeProperties_for_T.
    Definition Self (T : Ty.t) : Ty.t := T.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::mem::SizedTypeProperties"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_mem_SizedTypeProperties_for_T.
End mem.
