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

Module pin.
  (* StructRecord
    {
      name := "Pin";
      const_params := [];
      ty_params := [ "Ptr" ];
      fields := [ ("__pointer", Ptr) ];
    } *)
  
  Module Impl_core_marker_Copy_where_core_marker_Copy_Ptr_for_core_pin_Pin_Ptr.
    Definition Self (Ptr : Ty.t) : Ty.t := Ty.apply (Ty.path "core::pin::Pin") [] [ Ptr ].
    
    Axiom Implements :
      forall (Ptr : Ty.t),
      M.IsTraitInstance
        "core::marker::Copy"
        (Self Ptr)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_where_core_marker_Copy_Ptr_for_core_pin_Pin_Ptr.
  
  Module Impl_core_clone_Clone_where_core_clone_Clone_Ptr_for_core_pin_Pin_Ptr.
    Definition Self (Ptr : Ty.t) : Ty.t := Ty.apply (Ty.path "core::pin::Pin") [] [ Ptr ].
    
    (* Clone *)
    Definition clone (Ptr : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self Ptr in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.StructRecord
            "core::pin::Pin"
            [
              ("__pointer",
                M.call_closure (|
                  M.get_trait_method (| "core::clone::Clone", Ptr, [], "clone", [] |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::pin::Pin",
                      "__pointer"
                    |)
                  ]
                |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (Ptr : Ty.t),
      M.IsTraitInstance
        "core::clone::Clone"
        (Self Ptr)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("clone", InstanceField.Method (clone Ptr)) ].
  End Impl_core_clone_Clone_where_core_clone_Clone_Ptr_for_core_pin_Pin_Ptr.
  
  Module Impl_core_cmp_PartialEq_where_core_ops_deref_Deref_Ptr_where_core_ops_deref_Deref_Q_where_core_cmp_PartialEq_associated_type_associated_type_core_pin_Pin_Q_for_core_pin_Pin_Ptr.
    Definition Self (Ptr Q : Ty.t) : Ty.t := Ty.apply (Ty.path "core::pin::Pin") [] [ Ptr ].
    
    (*
        fn eq(&self, other: &Pin<Q>) -> bool {
            Ptr::Target::eq(self, other)
        }
    *)
    Definition eq (Ptr Q : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self Ptr Q in
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::cmp::PartialEq",
              Ty.associated,
              [ Ty.associated ],
              "eq",
              []
            |),
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::Deref",
                  Ty.apply (Ty.path "core::pin::Pin") [] [ Ptr ],
                  [],
                  "deref",
                  []
                |),
                [ M.read (| self |) ]
              |);
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::Deref",
                  Ty.apply (Ty.path "core::pin::Pin") [] [ Q ],
                  [],
                  "deref",
                  []
                |),
                [ M.read (| other |) ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn ne(&self, other: &Pin<Q>) -> bool {
            Ptr::Target::ne(self, other)
        }
    *)
    Definition ne (Ptr Q : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self Ptr Q in
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::cmp::PartialEq",
              Ty.associated,
              [ Ty.associated ],
              "ne",
              []
            |),
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::Deref",
                  Ty.apply (Ty.path "core::pin::Pin") [] [ Ptr ],
                  [],
                  "deref",
                  []
                |),
                [ M.read (| self |) ]
              |);
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::Deref",
                  Ty.apply (Ty.path "core::pin::Pin") [] [ Q ],
                  [],
                  "deref",
                  []
                |),
                [ M.read (| other |) ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (Ptr Q : Ty.t),
      M.IsTraitInstance
        "core::cmp::PartialEq"
        (Self Ptr Q)
        (* Trait polymorphic types *) [ (* Rhs *) Ty.apply (Ty.path "core::pin::Pin") [] [ Q ] ]
        (* Instance *)
        [ ("eq", InstanceField.Method (eq Ptr Q)); ("ne", InstanceField.Method (ne Ptr Q)) ].
  End Impl_core_cmp_PartialEq_where_core_ops_deref_Deref_Ptr_where_core_ops_deref_Deref_Q_where_core_cmp_PartialEq_associated_type_associated_type_core_pin_Pin_Q_for_core_pin_Pin_Ptr.
  
  Module Impl_core_cmp_Eq_where_core_ops_deref_Deref_Ptr_for_core_pin_Pin_Ptr.
    Definition Self (Ptr : Ty.t) : Ty.t := Ty.apply (Ty.path "core::pin::Pin") [] [ Ptr ].
    
    Axiom Implements :
      forall (Ptr : Ty.t),
      M.IsTraitInstance
        "core::cmp::Eq"
        (Self Ptr)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_cmp_Eq_where_core_ops_deref_Deref_Ptr_for_core_pin_Pin_Ptr.
  
  Module Impl_core_cmp_PartialOrd_where_core_ops_deref_Deref_Ptr_where_core_ops_deref_Deref_Q_where_core_cmp_PartialOrd_associated_type_associated_type_core_pin_Pin_Q_for_core_pin_Pin_Ptr.
    Definition Self (Ptr Q : Ty.t) : Ty.t := Ty.apply (Ty.path "core::pin::Pin") [] [ Ptr ].
    
    (*
        fn partial_cmp(&self, other: &Pin<Q>) -> Option<cmp::Ordering> {
            Ptr::Target::partial_cmp(self, other)
        }
    *)
    Definition partial_cmp
        (Ptr Q : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self Ptr Q in
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::cmp::PartialOrd",
              Ty.associated,
              [ Ty.associated ],
              "partial_cmp",
              []
            |),
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::Deref",
                  Ty.apply (Ty.path "core::pin::Pin") [] [ Ptr ],
                  [],
                  "deref",
                  []
                |),
                [ M.read (| self |) ]
              |);
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::Deref",
                  Ty.apply (Ty.path "core::pin::Pin") [] [ Q ],
                  [],
                  "deref",
                  []
                |),
                [ M.read (| other |) ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn lt(&self, other: &Pin<Q>) -> bool {
            Ptr::Target::lt(self, other)
        }
    *)
    Definition lt (Ptr Q : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self Ptr Q in
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::cmp::PartialOrd",
              Ty.associated,
              [ Ty.associated ],
              "lt",
              []
            |),
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::Deref",
                  Ty.apply (Ty.path "core::pin::Pin") [] [ Ptr ],
                  [],
                  "deref",
                  []
                |),
                [ M.read (| self |) ]
              |);
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::Deref",
                  Ty.apply (Ty.path "core::pin::Pin") [] [ Q ],
                  [],
                  "deref",
                  []
                |),
                [ M.read (| other |) ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn le(&self, other: &Pin<Q>) -> bool {
            Ptr::Target::le(self, other)
        }
    *)
    Definition le (Ptr Q : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self Ptr Q in
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::cmp::PartialOrd",
              Ty.associated,
              [ Ty.associated ],
              "le",
              []
            |),
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::Deref",
                  Ty.apply (Ty.path "core::pin::Pin") [] [ Ptr ],
                  [],
                  "deref",
                  []
                |),
                [ M.read (| self |) ]
              |);
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::Deref",
                  Ty.apply (Ty.path "core::pin::Pin") [] [ Q ],
                  [],
                  "deref",
                  []
                |),
                [ M.read (| other |) ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn gt(&self, other: &Pin<Q>) -> bool {
            Ptr::Target::gt(self, other)
        }
    *)
    Definition gt (Ptr Q : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self Ptr Q in
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::cmp::PartialOrd",
              Ty.associated,
              [ Ty.associated ],
              "gt",
              []
            |),
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::Deref",
                  Ty.apply (Ty.path "core::pin::Pin") [] [ Ptr ],
                  [],
                  "deref",
                  []
                |),
                [ M.read (| self |) ]
              |);
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::Deref",
                  Ty.apply (Ty.path "core::pin::Pin") [] [ Q ],
                  [],
                  "deref",
                  []
                |),
                [ M.read (| other |) ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn ge(&self, other: &Pin<Q>) -> bool {
            Ptr::Target::ge(self, other)
        }
    *)
    Definition ge (Ptr Q : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self Ptr Q in
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::cmp::PartialOrd",
              Ty.associated,
              [ Ty.associated ],
              "ge",
              []
            |),
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::Deref",
                  Ty.apply (Ty.path "core::pin::Pin") [] [ Ptr ],
                  [],
                  "deref",
                  []
                |),
                [ M.read (| self |) ]
              |);
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::Deref",
                  Ty.apply (Ty.path "core::pin::Pin") [] [ Q ],
                  [],
                  "deref",
                  []
                |),
                [ M.read (| other |) ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (Ptr Q : Ty.t),
      M.IsTraitInstance
        "core::cmp::PartialOrd"
        (Self Ptr Q)
        (* Trait polymorphic types *) [ (* Rhs *) Ty.apply (Ty.path "core::pin::Pin") [] [ Q ] ]
        (* Instance *)
        [
          ("partial_cmp", InstanceField.Method (partial_cmp Ptr Q));
          ("lt", InstanceField.Method (lt Ptr Q));
          ("le", InstanceField.Method (le Ptr Q));
          ("gt", InstanceField.Method (gt Ptr Q));
          ("ge", InstanceField.Method (ge Ptr Q))
        ].
  End Impl_core_cmp_PartialOrd_where_core_ops_deref_Deref_Ptr_where_core_ops_deref_Deref_Q_where_core_cmp_PartialOrd_associated_type_associated_type_core_pin_Pin_Q_for_core_pin_Pin_Ptr.
  
  Module Impl_core_cmp_Ord_where_core_ops_deref_Deref_Ptr_for_core_pin_Pin_Ptr.
    Definition Self (Ptr : Ty.t) : Ty.t := Ty.apply (Ty.path "core::pin::Pin") [] [ Ptr ].
    
    (*
        fn cmp(&self, other: &Self) -> cmp::Ordering {
            Ptr::Target::cmp(self, other)
        }
    *)
    Definition cmp (Ptr : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self Ptr in
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.call_closure (|
            M.get_trait_method (| "core::cmp::Ord", Ty.associated, [], "cmp", [] |),
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::Deref",
                  Ty.apply (Ty.path "core::pin::Pin") [] [ Ptr ],
                  [],
                  "deref",
                  []
                |),
                [ M.read (| self |) ]
              |);
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::Deref",
                  Ty.apply (Ty.path "core::pin::Pin") [] [ Ptr ],
                  [],
                  "deref",
                  []
                |),
                [ M.read (| other |) ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (Ptr : Ty.t),
      M.IsTraitInstance
        "core::cmp::Ord"
        (Self Ptr)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("cmp", InstanceField.Method (cmp Ptr)) ].
  End Impl_core_cmp_Ord_where_core_ops_deref_Deref_Ptr_for_core_pin_Pin_Ptr.
  
  Module Impl_core_hash_Hash_where_core_ops_deref_Deref_Ptr_for_core_pin_Pin_Ptr.
    Definition Self (Ptr : Ty.t) : Ty.t := Ty.apply (Ty.path "core::pin::Pin") [] [ Ptr ].
    
    (*
        fn hash<H: Hasher>(&self, state: &mut H) {
            Ptr::Target::hash(self, state);
        }
    *)
    Definition hash (Ptr : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self Ptr 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.call_closure (|
                      M.get_trait_method (|
                        "core::ops::deref::Deref",
                        Ty.apply (Ty.path "core::pin::Pin") [] [ Ptr ],
                        [],
                        "deref",
                        []
                      |),
                      [ M.read (| self |) ]
                    |);
                    M.read (| state |)
                  ]
                |)
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (Ptr : Ty.t),
      M.IsTraitInstance
        "core::hash::Hash"
        (Self Ptr)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("hash", InstanceField.Method (hash Ptr)) ].
  End Impl_core_hash_Hash_where_core_ops_deref_Deref_Ptr_for_core_pin_Pin_Ptr.
  
  Module Impl_core_pin_Pin_Ptr.
    Definition Self (Ptr : Ty.t) : Ty.t := Ty.apply (Ty.path "core::pin::Pin") [] [ Ptr ].
    
    (*
        pub const fn new(pointer: Ptr) -> Pin<Ptr> {
            // SAFETY: the value pointed to is `Unpin`, and so has no requirements
            // around pinning.
            unsafe { Pin::new_unchecked(pointer) }
        }
    *)
    Definition new (Ptr : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self Ptr in
      match ε, τ, α with
      | [], [], [ pointer ] =>
        ltac:(M.monadic
          (let pointer := M.alloc (| pointer |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::pin::Pin") [] [ Ptr ],
              "new_unchecked",
              []
            |),
            [ M.read (| pointer |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_new :
      forall (Ptr : Ty.t),
      M.IsAssociatedFunction (Self Ptr) "new" (new Ptr).
    
    (*
        pub const fn into_inner(pin: Pin<Ptr>) -> Ptr {
            pin.__pointer
        }
    *)
    Definition into_inner (Ptr : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self Ptr in
      match ε, τ, α with
      | [], [], [ pin ] =>
        ltac:(M.monadic
          (let pin := M.alloc (| pin |) in
          M.read (|
            M.SubPointer.get_struct_record_field (| pin, "core::pin::Pin", "__pointer" |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_into_inner :
      forall (Ptr : Ty.t),
      M.IsAssociatedFunction (Self Ptr) "into_inner" (into_inner Ptr).
    (*
        pub const unsafe fn new_unchecked(pointer: Ptr) -> Pin<Ptr> {
            Pin { __pointer: pointer }
        }
    *)
    Definition new_unchecked
        (Ptr : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self Ptr in
      match ε, τ, α with
      | [], [], [ pointer ] =>
        ltac:(M.monadic
          (let pointer := M.alloc (| pointer |) in
          Value.StructRecord "core::pin::Pin" [ ("__pointer", M.read (| pointer |)) ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_new_unchecked :
      forall (Ptr : Ty.t),
      M.IsAssociatedFunction (Self Ptr) "new_unchecked" (new_unchecked Ptr).
    
    (*
        pub fn as_ref(&self) -> Pin<&Ptr::Target> {
            // SAFETY: see documentation on this function
            unsafe { Pin::new_unchecked(&*self.__pointer) }
        }
    *)
    Definition as_ref (Ptr : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self Ptr in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply
                (Ty.path "core::pin::Pin")
                []
                [ Ty.apply (Ty.path "&") [] [ Ty.associated ] ],
              "new_unchecked",
              []
            |),
            [
              M.call_closure (|
                M.get_trait_method (| "core::ops::deref::Deref", Ptr, [], "deref", [] |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::pin::Pin",
                    "__pointer"
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_as_ref :
      forall (Ptr : Ty.t),
      M.IsAssociatedFunction (Self Ptr) "as_ref" (as_ref Ptr).
    (*
        pub fn as_mut(&mut self) -> Pin<&mut Ptr::Target> {
            // SAFETY: see documentation on this function
            unsafe { Pin::new_unchecked(&mut *self.__pointer) }
        }
    *)
    Definition as_mut (Ptr : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self Ptr in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply
                (Ty.path "core::pin::Pin")
                []
                [ Ty.apply (Ty.path "&mut") [] [ Ty.associated ] ],
              "new_unchecked",
              []
            |),
            [
              M.call_closure (|
                M.get_trait_method (| "core::ops::deref::DerefMut", Ptr, [], "deref_mut", [] |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::pin::Pin",
                    "__pointer"
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_as_mut :
      forall (Ptr : Ty.t),
      M.IsAssociatedFunction (Self Ptr) "as_mut" (as_mut Ptr).
    
    (*
        pub fn as_deref_mut(self: Pin<&mut Pin<Ptr>>) -> Pin<&mut Ptr::Target> {
            // SAFETY: What we're asserting here is that going from
            //
            //     Pin<&mut Pin<Ptr>>
            //
            // to
            //
            //     Pin<&mut Ptr::Target>
            //
            // is safe.
            //
            // We need to ensure that two things hold for that to be the case:
            //
            // 1) Once we give out a `Pin<&mut Ptr::Target>`, a `&mut Ptr::Target` will not be given out.
            // 2) By giving out a `Pin<&mut Ptr::Target>`, we do not risk violating
            // `Pin<&mut Pin<Ptr>>`
            //
            // The existence of `Pin<Ptr>` is sufficient to guarantee #1: since we already have a
            // `Pin<Ptr>`, it must already uphold the pinning guarantees, which must mean that
            // `Pin<&mut Ptr::Target>` does as well, since `Pin::as_mut` is safe. We do not have to rely
            // on the fact that `Ptr` is _also_ pinned.
            //
            // For #2, we need to ensure that code given a `Pin<&mut Ptr::Target>` cannot cause the
            // `Pin<Ptr>` to move? That is not possible, since `Pin<&mut Ptr::Target>` no longer retains
            // any access to the `Ptr` itself, much less the `Pin<Ptr>`.
            unsafe { self.get_unchecked_mut() }.as_mut()
        }
    *)
    Definition as_deref_mut
        (Ptr : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self Ptr in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::pin::Pin") [] [ Ptr ],
              "as_mut",
              []
            |),
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "core::pin::Pin")
                    []
                    [
                      Ty.apply
                        (Ty.path "&mut")
                        []
                        [ Ty.apply (Ty.path "core::pin::Pin") [] [ Ptr ] ]
                    ],
                  "get_unchecked_mut",
                  []
                |),
                [ M.read (| self |) ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_as_deref_mut :
      forall (Ptr : Ty.t),
      M.IsAssociatedFunction (Self Ptr) "as_deref_mut" (as_deref_mut Ptr).
    
    (*
        pub fn set(&mut self, value: Ptr::Target)
        where
            Ptr::Target: Sized,
        {
            *(self.__pointer) = value;
        }
    *)
    Definition set (Ptr : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self Ptr in
      match ε, τ, α with
      | [], [], [ self; value ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let value := M.alloc (| value |) in
          M.read (|
            let~ _ :=
              M.write (|
                M.call_closure (|
                  M.get_trait_method (| "core::ops::deref::DerefMut", Ptr, [], "deref_mut", [] |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::pin::Pin",
                      "__pointer"
                    |)
                  ]
                |),
                M.read (| value |)
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_set :
      forall (Ptr : Ty.t),
      M.IsAssociatedFunction (Self Ptr) "set" (set Ptr).
    (*
        pub const unsafe fn into_inner_unchecked(pin: Pin<Ptr>) -> Ptr {
            pin.__pointer
        }
    *)
    Definition into_inner_unchecked
        (Ptr : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self Ptr in
      match ε, τ, α with
      | [], [], [ pin ] =>
        ltac:(M.monadic
          (let pin := M.alloc (| pin |) in
          M.read (|
            M.SubPointer.get_struct_record_field (| pin, "core::pin::Pin", "__pointer" |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_into_inner_unchecked :
      forall (Ptr : Ty.t),
      M.IsAssociatedFunction (Self Ptr) "into_inner_unchecked" (into_inner_unchecked Ptr).
  End Impl_core_pin_Pin_Ptr.
  
  
  
  
  Module Impl_core_pin_Pin_ref__T.
    Definition Self (T : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "core::pin::Pin") [] [ Ty.apply (Ty.path "&") [] [ T ] ].
    
    (*
        pub unsafe fn map_unchecked<U, F>(self, func: F) -> Pin<&'a U>
        where
            U: ?Sized,
            F: FnOnce(&T) -> &U,
        {
            let pointer = &*self.__pointer;
            let new_pointer = func(pointer);
    
            // SAFETY: the safety contract for `new_unchecked` must be
            // upheld by the caller.
            unsafe { Pin::new_unchecked(new_pointer) }
        }
    *)
    Definition map_unchecked (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [ U; F ], [ self; func ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let func := M.alloc (| func |) in
          M.read (|
            let~ pointer :=
              M.alloc (|
                M.read (|
                  M.SubPointer.get_struct_record_field (| self, "core::pin::Pin", "__pointer" |)
                |)
              |) in
            let~ new_pointer :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::function::FnOnce",
                    F,
                    [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ T ] ] ],
                    "call_once",
                    []
                  |),
                  [ M.read (| func |); Value.Tuple [ M.read (| pointer |) ] ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::pin::Pin") [] [ Ty.apply (Ty.path "&") [] [ U ] ],
                  "new_unchecked",
                  []
                |),
                [ M.read (| new_pointer |) ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_map_unchecked :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "map_unchecked" (map_unchecked T).
    
    (*
        pub const fn get_ref(self) -> &'a T {
            self.__pointer
        }
    *)
    Definition get_ref (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.SubPointer.get_struct_record_field (| self, "core::pin::Pin", "__pointer" |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_get_ref :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "get_ref" (get_ref T).
    (*
        pub const fn static_ref(r: &'static T) -> Pin<&'static T> {
            // SAFETY: The 'static borrow guarantees the data will not be
            // moved/invalidated until it gets dropped (which is never).
            unsafe { Pin::new_unchecked(r) }
        }
    *)
    Definition static_ref (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ r ] =>
        ltac:(M.monadic
          (let r := M.alloc (| r |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::pin::Pin") [] [ Ty.apply (Ty.path "&") [] [ T ] ],
              "new_unchecked",
              []
            |),
            [ M.read (| r |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_static_ref :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "static_ref" (static_ref T).
  End Impl_core_pin_Pin_ref__T.
  
  Module Impl_core_pin_Pin_ref_mut_T.
    Definition Self (T : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "core::pin::Pin") [] [ Ty.apply (Ty.path "&mut") [] [ T ] ].
    
    (*
        pub const fn into_ref(self) -> Pin<&'a T> {
            Pin { __pointer: self.__pointer }
        }
    *)
    Definition into_ref (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
          Value.StructRecord
            "core::pin::Pin"
            [
              ("__pointer",
                M.read (|
                  M.SubPointer.get_struct_record_field (| self, "core::pin::Pin", "__pointer" |)
                |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_into_ref :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "into_ref" (into_ref T).
    
    (*
        pub const fn get_mut(self) -> &'a mut T
        where
            T: Unpin,
        {
            self.__pointer
        }
    *)
    Definition get_mut (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.SubPointer.get_struct_record_field (| self, "core::pin::Pin", "__pointer" |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_get_mut :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "get_mut" (get_mut T).
    
    (*
        pub const unsafe fn get_unchecked_mut(self) -> &'a mut T {
            self.__pointer
        }
    *)
    Definition get_unchecked_mut
        (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.SubPointer.get_struct_record_field (| self, "core::pin::Pin", "__pointer" |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_get_unchecked_mut :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "get_unchecked_mut" (get_unchecked_mut T).
    
    (*
        pub unsafe fn map_unchecked_mut<U, F>(self, func: F) -> Pin<&'a mut U>
        where
            U: ?Sized,
            F: FnOnce(&mut T) -> &mut U,
        {
            // SAFETY: the caller is responsible for not moving the
            // value out of this reference.
            let pointer = unsafe { Pin::get_unchecked_mut(self) };
            let new_pointer = func(pointer);
            // SAFETY: as the value of `this` is guaranteed to not have
            // been moved out, this call to `new_unchecked` is safe.
            unsafe { Pin::new_unchecked(new_pointer) }
        }
    *)
    Definition map_unchecked_mut
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [ U; F ], [ self; func ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let func := M.alloc (| func |) in
          M.read (|
            let~ pointer :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::pin::Pin") [] [ Ty.apply (Ty.path "&mut") [] [ T ] ],
                    "get_unchecked_mut",
                    []
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            let~ new_pointer :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::function::FnOnce",
                    F,
                    [ Ty.tuple [ Ty.apply (Ty.path "&mut") [] [ T ] ] ],
                    "call_once",
                    []
                  |),
                  [ M.read (| func |); Value.Tuple [ M.read (| pointer |) ] ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::pin::Pin") [] [ Ty.apply (Ty.path "&mut") [] [ U ] ],
                  "new_unchecked",
                  []
                |),
                [ M.read (| new_pointer |) ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_map_unchecked_mut :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "map_unchecked_mut" (map_unchecked_mut T).
    (*
        pub const fn static_mut(r: &'static mut T) -> Pin<&'static mut T> {
            // SAFETY: The 'static borrow guarantees the data will not be
            // moved/invalidated until it gets dropped (which is never).
            unsafe { Pin::new_unchecked(r) }
        }
    *)
    Definition static_mut (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ r ] =>
        ltac:(M.monadic
          (let r := M.alloc (| r |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::pin::Pin") [] [ Ty.apply (Ty.path "&mut") [] [ T ] ],
              "new_unchecked",
              []
            |),
            [ M.read (| r |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_static_mut :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "static_mut" (static_mut T).
  End Impl_core_pin_Pin_ref_mut_T.
  
  
  
  Module Impl_core_ops_deref_Deref_where_core_ops_deref_Deref_Ptr_for_core_pin_Pin_Ptr.
    Definition Self (Ptr : Ty.t) : Ty.t := Ty.apply (Ty.path "core::pin::Pin") [] [ Ptr ].
    
    (*     type Target = Ptr::Target; *)
    Definition _Target (Ptr : Ty.t) : Ty.t := Ty.associated.
    
    (*
        fn deref(&self) -> &Ptr::Target {
            Pin::get_ref(Pin::as_ref(self))
        }
    *)
    Definition deref (Ptr : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self Ptr in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply
                (Ty.path "core::pin::Pin")
                []
                [ Ty.apply (Ty.path "&") [] [ Ty.associated ] ],
              "get_ref",
              []
            |),
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::pin::Pin") [] [ Ptr ],
                  "as_ref",
                  []
                |),
                [ M.read (| self |) ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (Ptr : Ty.t),
      M.IsTraitInstance
        "core::ops::deref::Deref"
        (Self Ptr)
        (* Trait polymorphic types *) []
        (* Instance *)
        [ ("Target", InstanceField.Ty (_Target Ptr)); ("deref", InstanceField.Method (deref Ptr)) ].
  End Impl_core_ops_deref_Deref_where_core_ops_deref_Deref_Ptr_for_core_pin_Pin_Ptr.
  
  Module Impl_core_ops_deref_DerefMut_where_core_ops_deref_DerefMut_Ptr_for_core_pin_Pin_Ptr.
    Definition Self (Ptr : Ty.t) : Ty.t := Ty.apply (Ty.path "core::pin::Pin") [] [ Ptr ].
    
    (*
        fn deref_mut(&mut self) -> &mut Ptr::Target {
            Pin::get_mut(Pin::as_mut(self))
        }
    *)
    Definition deref_mut (Ptr : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self Ptr in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply
                (Ty.path "core::pin::Pin")
                []
                [ Ty.apply (Ty.path "&mut") [] [ Ty.associated ] ],
              "get_mut",
              []
            |),
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::pin::Pin") [] [ Ptr ],
                  "as_mut",
                  []
                |),
                [ M.read (| self |) ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (Ptr : Ty.t),
      M.IsTraitInstance
        "core::ops::deref::DerefMut"
        (Self Ptr)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("deref_mut", InstanceField.Method (deref_mut Ptr)) ].
  End Impl_core_ops_deref_DerefMut_where_core_ops_deref_DerefMut_Ptr_for_core_pin_Pin_Ptr.
  
  Module Impl_core_ops_deref_DerefPure_where_core_ops_deref_DerefPure_Ptr_for_core_pin_Pin_Ptr.
    Definition Self (Ptr : Ty.t) : Ty.t := Ty.apply (Ty.path "core::pin::Pin") [] [ Ptr ].
    
    Axiom Implements :
      forall (Ptr : Ty.t),
      M.IsTraitInstance
        "core::ops::deref::DerefPure"
        (Self Ptr)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_ops_deref_DerefPure_where_core_ops_deref_DerefPure_Ptr_for_core_pin_Pin_Ptr.
  
  Module Impl_core_ops_deref_Receiver_where_core_ops_deref_Receiver_Ptr_for_core_pin_Pin_Ptr.
    Definition Self (Ptr : Ty.t) : Ty.t := Ty.apply (Ty.path "core::pin::Pin") [] [ Ptr ].
    
    Axiom Implements :
      forall (Ptr : Ty.t),
      M.IsTraitInstance
        "core::ops::deref::Receiver"
        (Self Ptr)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_ops_deref_Receiver_where_core_ops_deref_Receiver_Ptr_for_core_pin_Pin_Ptr.
  
  Module Impl_core_fmt_Debug_where_core_fmt_Debug_Ptr_for_core_pin_Pin_Ptr.
    Definition Self (Ptr : Ty.t) : Ty.t := Ty.apply (Ty.path "core::pin::Pin") [] [ Ptr ].
    
    (*
        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
            fmt::Debug::fmt(&self.__pointer, f)
        }
    *)
    Definition fmt (Ptr : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self Ptr in
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_trait_method (| "core::fmt::Debug", Ptr, [], "fmt", [] |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::pin::Pin",
                "__pointer"
              |);
              M.read (| f |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (Ptr : Ty.t),
      M.IsTraitInstance
        "core::fmt::Debug"
        (Self Ptr)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method (fmt Ptr)) ].
  End Impl_core_fmt_Debug_where_core_fmt_Debug_Ptr_for_core_pin_Pin_Ptr.
  
  Module Impl_core_fmt_Display_where_core_fmt_Display_Ptr_for_core_pin_Pin_Ptr.
    Definition Self (Ptr : Ty.t) : Ty.t := Ty.apply (Ty.path "core::pin::Pin") [] [ Ptr ].
    
    (*
        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
            fmt::Display::fmt(&self.__pointer, f)
        }
    *)
    Definition fmt (Ptr : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self Ptr in
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_trait_method (| "core::fmt::Display", Ptr, [], "fmt", [] |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::pin::Pin",
                "__pointer"
              |);
              M.read (| f |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (Ptr : Ty.t),
      M.IsTraitInstance
        "core::fmt::Display"
        (Self Ptr)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method (fmt Ptr)) ].
  End Impl_core_fmt_Display_where_core_fmt_Display_Ptr_for_core_pin_Pin_Ptr.
  
  Module Impl_core_fmt_Pointer_where_core_fmt_Pointer_Ptr_for_core_pin_Pin_Ptr.
    Definition Self (Ptr : Ty.t) : Ty.t := Ty.apply (Ty.path "core::pin::Pin") [] [ Ptr ].
    
    (*
        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
            fmt::Pointer::fmt(&self.__pointer, f)
        }
    *)
    Definition fmt (Ptr : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self Ptr in
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_trait_method (| "core::fmt::Pointer", Ptr, [], "fmt", [] |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::pin::Pin",
                "__pointer"
              |);
              M.read (| f |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (Ptr : Ty.t),
      M.IsTraitInstance
        "core::fmt::Pointer"
        (Self Ptr)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method (fmt Ptr)) ].
  End Impl_core_fmt_Pointer_where_core_fmt_Pointer_Ptr_for_core_pin_Pin_Ptr.
  
  Module Impl_core_ops_unsize_CoerceUnsized_where_core_ops_unsize_CoerceUnsized_Ptr_U_where_core_pin_PinCoerceUnsized_Ptr_where_core_pin_PinCoerceUnsized_U_core_pin_Pin_U_for_core_pin_Pin_Ptr.
    Definition Self (Ptr U : Ty.t) : Ty.t := Ty.apply (Ty.path "core::pin::Pin") [] [ Ptr ].
    
    Axiom Implements :
      forall (Ptr U : Ty.t),
      M.IsTraitInstance
        "core::ops::unsize::CoerceUnsized"
        (Self Ptr U)
        (* Trait polymorphic types *) [ (* T *) Ty.apply (Ty.path "core::pin::Pin") [] [ U ] ]
        (* Instance *) [].
  End Impl_core_ops_unsize_CoerceUnsized_where_core_ops_unsize_CoerceUnsized_Ptr_U_where_core_pin_PinCoerceUnsized_Ptr_where_core_pin_PinCoerceUnsized_U_core_pin_Pin_U_for_core_pin_Pin_Ptr.
  
  Module Impl_core_ops_unsize_DispatchFromDyn_where_core_ops_unsize_DispatchFromDyn_Ptr_U_where_core_pin_PinCoerceUnsized_Ptr_where_core_pin_PinCoerceUnsized_U_core_pin_Pin_U_for_core_pin_Pin_Ptr.
    Definition Self (Ptr U : Ty.t) : Ty.t := Ty.apply (Ty.path "core::pin::Pin") [] [ Ptr ].
    
    Axiom Implements :
      forall (Ptr U : Ty.t),
      M.IsTraitInstance
        "core::ops::unsize::DispatchFromDyn"
        (Self Ptr U)
        (* Trait polymorphic types *) [ (* T *) Ty.apply (Ty.path "core::pin::Pin") [] [ U ] ]
        (* Instance *) [].
  End Impl_core_ops_unsize_DispatchFromDyn_where_core_ops_unsize_DispatchFromDyn_Ptr_U_where_core_pin_PinCoerceUnsized_Ptr_where_core_pin_PinCoerceUnsized_U_core_pin_Pin_U_for_core_pin_Pin_Ptr.
  
  (* Trait *)
  (* Empty module 'PinCoerceUnsized' *)
  
  Module Impl_core_pin_PinCoerceUnsized_where_core_marker_Sized_T_for_ref__T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "&") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::pin::PinCoerceUnsized"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_pin_PinCoerceUnsized_where_core_marker_Sized_T_for_ref__T.
  
  Module Impl_core_pin_PinCoerceUnsized_where_core_marker_Sized_T_for_ref_mut_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "&mut") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::pin::PinCoerceUnsized"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_pin_PinCoerceUnsized_where_core_marker_Sized_T_for_ref_mut_T.
  
  Module Impl_core_pin_PinCoerceUnsized_where_core_pin_PinCoerceUnsized_T_for_core_pin_Pin_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::pin::Pin") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::pin::PinCoerceUnsized"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_pin_PinCoerceUnsized_where_core_pin_PinCoerceUnsized_T_for_core_pin_Pin_T.
  
  Module Impl_core_pin_PinCoerceUnsized_where_core_marker_Sized_T_for_pointer_const_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "*const") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::pin::PinCoerceUnsized"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_pin_PinCoerceUnsized_where_core_marker_Sized_T_for_pointer_const_T.
  
  Module Impl_core_pin_PinCoerceUnsized_where_core_marker_Sized_T_for_pointer_mut_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "*mut") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::pin::PinCoerceUnsized"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_pin_PinCoerceUnsized_where_core_marker_Sized_T_for_pointer_mut_T.
End pin.
