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

Module ops.
  Module deref.
    (* Trait *)
    (* Empty module 'Deref' *)
    
    Module Impl_core_ops_deref_Deref_where_core_marker_Sized_T_for_ref__T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "&") [] [ T ].
      
      (*     type Target = T; *)
      Definition _Target (T : Ty.t) : Ty.t := T.
      
      (*
          fn deref(&self) -> &T {
              *self
          }
      *)
      Definition deref (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::ops::deref::Deref"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Target", InstanceField.Ty (_Target T)); ("deref", InstanceField.Method (deref T)) ].
    End Impl_core_ops_deref_Deref_where_core_marker_Sized_T_for_ref__T.
    
    Module Impl_core_ops_deref_DerefMut_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::ops::deref::DerefMut"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_ops_deref_DerefMut_where_core_marker_Sized_T_for_ref__T.
    
    Module Impl_core_ops_deref_Deref_where_core_marker_Sized_T_for_ref_mut_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "&mut") [] [ T ].
      
      (*     type Target = T; *)
      Definition _Target (T : Ty.t) : Ty.t := T.
      
      (*
          fn deref(&self) -> &T {
              *self
          }
      *)
      Definition deref (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::ops::deref::Deref"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Target", InstanceField.Ty (_Target T)); ("deref", InstanceField.Method (deref T)) ].
    End Impl_core_ops_deref_Deref_where_core_marker_Sized_T_for_ref_mut_T.
    
    (* Trait *)
    (* Empty module 'DerefMut' *)
    
    Module Impl_core_ops_deref_DerefMut_where_core_marker_Sized_T_for_ref_mut_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "&mut") [] [ T ].
      
      (*
          fn deref_mut(&mut self) -> &mut T {
              *self
          }
      *)
      Definition deref_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.read (| self |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::ops::deref::DerefMut"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("deref_mut", InstanceField.Method (deref_mut T)) ].
    End Impl_core_ops_deref_DerefMut_where_core_marker_Sized_T_for_ref_mut_T.
    
    (* Trait *)
    (* Empty module 'DerefPure' *)
    
    Module Impl_core_ops_deref_DerefPure_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::ops::deref::DerefPure"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_ops_deref_DerefPure_where_core_marker_Sized_T_for_ref__T.
    
    Module Impl_core_ops_deref_DerefPure_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::ops::deref::DerefPure"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_ops_deref_DerefPure_where_core_marker_Sized_T_for_ref_mut_T.
    
    (* Trait *)
    (* Empty module 'Receiver' *)
    
    Module Impl_core_ops_deref_Receiver_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::ops::deref::Receiver"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_ops_deref_Receiver_where_core_marker_Sized_T_for_ref__T.
    
    Module Impl_core_ops_deref_Receiver_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::ops::deref::Receiver"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_ops_deref_Receiver_where_core_marker_Sized_T_for_ref_mut_T.
  End deref.
End ops.
