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

Module borrow.
  (* Trait *)
  (* Empty module 'Borrow' *)
  
  (* Trait *)
  (* Empty module 'BorrowMut' *)
  
  Module Impl_core_borrow_Borrow_where_core_marker_Sized_T_T_for_T.
    Definition Self (T : Ty.t) : Ty.t := T.
    
    (*
        fn borrow(&self) -> &T {
            self
        }
    *)
    Definition borrow (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 (| self |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::borrow::Borrow"
        (Self T)
        (* Trait polymorphic types *) [ (* Borrowed *) T ]
        (* Instance *) [ ("borrow", InstanceField.Method (borrow T)) ].
  End Impl_core_borrow_Borrow_where_core_marker_Sized_T_T_for_T.
  
  Module Impl_core_borrow_BorrowMut_where_core_marker_Sized_T_T_for_T.
    Definition Self (T : Ty.t) : Ty.t := T.
    
    (*
        fn borrow_mut(&mut self) -> &mut T {
            self
        }
    *)
    Definition borrow_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 (| self |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::borrow::BorrowMut"
        (Self T)
        (* Trait polymorphic types *) [ (* Borrowed *) T ]
        (* Instance *) [ ("borrow_mut", InstanceField.Method (borrow_mut T)) ].
  End Impl_core_borrow_BorrowMut_where_core_marker_Sized_T_T_for_T.
  
  Module Impl_core_borrow_Borrow_where_core_marker_Sized_T_T_for_ref__T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "&") [] [ T ].
    
    (*
        fn borrow(&self) -> &T {
            &**self
        }
    *)
    Definition borrow (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::borrow::Borrow"
        (Self T)
        (* Trait polymorphic types *) [ (* Borrowed *) T ]
        (* Instance *) [ ("borrow", InstanceField.Method (borrow T)) ].
  End Impl_core_borrow_Borrow_where_core_marker_Sized_T_T_for_ref__T.
  
  Module Impl_core_borrow_Borrow_where_core_marker_Sized_T_T_for_ref_mut_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "&mut") [] [ T ].
    
    (*
        fn borrow(&self) -> &T {
            &**self
        }
    *)
    Definition borrow (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::borrow::Borrow"
        (Self T)
        (* Trait polymorphic types *) [ (* Borrowed *) T ]
        (* Instance *) [ ("borrow", InstanceField.Method (borrow T)) ].
  End Impl_core_borrow_Borrow_where_core_marker_Sized_T_T_for_ref_mut_T.
  
  Module Impl_core_borrow_BorrowMut_where_core_marker_Sized_T_T_for_ref_mut_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "&mut") [] [ T ].
    
    (*
        fn borrow_mut(&mut self) -> &mut T {
            &mut **self
        }
    *)
    Definition borrow_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::borrow::BorrowMut"
        (Self T)
        (* Trait polymorphic types *) [ (* Borrowed *) T ]
        (* Instance *) [ ("borrow_mut", InstanceField.Method (borrow_mut T)) ].
  End Impl_core_borrow_BorrowMut_where_core_marker_Sized_T_T_for_ref_mut_T.
End borrow.
