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

Module vec.
  Module cow.
    Module Impl_core_convert_From_where_core_clone_Clone_T_ref__slice_T_for_alloc_borrow_Cow_slice_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::borrow::Cow") [] [ Ty.apply (Ty.path "slice") [] [ T ] ].
      
      (*
          fn from(s: &'a [T]) -> Cow<'a, [T]> {
              Cow::Borrowed(s)
          }
      *)
      Definition from (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ s ] =>
          ltac:(M.monadic
            (let s := M.alloc (| s |) in
            Value.StructTuple "alloc::borrow::Cow::Borrowed" [ M.read (| s |) ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::convert::From"
          (Self T)
          (* Trait polymorphic types *)
          [ (* T *) Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ T ] ] ]
          (* Instance *) [ ("from", InstanceField.Method (from T)) ].
    End Impl_core_convert_From_where_core_clone_Clone_T_ref__slice_T_for_alloc_borrow_Cow_slice_T.
    
    Module Impl_core_convert_From_where_core_clone_Clone_T_ref__array_N_T_for_alloc_borrow_Cow_slice_T.
      Definition Self (N : Value.t) (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::borrow::Cow") [] [ Ty.apply (Ty.path "slice") [] [ T ] ].
      
      (*
          fn from(s: &'a [T; N]) -> Cow<'a, [T]> {
              Cow::Borrowed(s as &[_])
          }
      *)
      Definition from
          (N : Value.t)
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self N T in
        match ε, τ, α with
        | [], [], [ s ] =>
          ltac:(M.monadic
            (let s := M.alloc (| s |) in
            Value.StructTuple
              "alloc::borrow::Cow::Borrowed"
              [ M.read (| M.use (M.alloc (| M.read (| s |) |)) |) ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (N : Value.t) (T : Ty.t),
        M.IsTraitInstance
          "core::convert::From"
          (Self N T)
          (* Trait polymorphic types *)
          [ (* T *) Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "array") [ N ] [ T ] ] ]
          (* Instance *) [ ("from", InstanceField.Method (from N T)) ].
    End Impl_core_convert_From_where_core_clone_Clone_T_ref__array_N_T_for_alloc_borrow_Cow_slice_T.
    
    Module Impl_core_convert_From_where_core_clone_Clone_T_alloc_vec_Vec_T_alloc_alloc_Global_for_alloc_borrow_Cow_slice_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::borrow::Cow") [] [ Ty.apply (Ty.path "slice") [] [ T ] ].
      
      (*
          fn from(v: Vec<T>) -> Cow<'a, [T]> {
              Cow::Owned(v)
          }
      *)
      Definition from (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ v ] =>
          ltac:(M.monadic
            (let v := M.alloc (| v |) in
            Value.StructTuple "alloc::borrow::Cow::Owned" [ M.read (| v |) ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::convert::From"
          (Self T)
          (* Trait polymorphic types *)
          [ (* T *) Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; Ty.path "alloc::alloc::Global" ] ]
          (* Instance *) [ ("from", InstanceField.Method (from T)) ].
    End Impl_core_convert_From_where_core_clone_Clone_T_alloc_vec_Vec_T_alloc_alloc_Global_for_alloc_borrow_Cow_slice_T.
    
    Module Impl_core_convert_From_where_core_clone_Clone_T_ref__alloc_vec_Vec_T_alloc_alloc_Global_for_alloc_borrow_Cow_slice_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::borrow::Cow") [] [ Ty.apply (Ty.path "slice") [] [ T ] ].
      
      (*
          fn from(v: &'a Vec<T>) -> Cow<'a, [T]> {
              Cow::Borrowed(v.as_slice())
          }
      *)
      Definition from (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ v ] =>
          ltac:(M.monadic
            (let v := M.alloc (| v |) in
            Value.StructTuple
              "alloc::borrow::Cow::Borrowed"
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; Ty.path "alloc::alloc::Global" ],
                    "as_slice",
                    []
                  |),
                  [ M.read (| v |) ]
                |)
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::convert::From"
          (Self T)
          (* Trait polymorphic types *)
          [
            (* T *)
            Ty.apply
              (Ty.path "&")
              []
              [ Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; Ty.path "alloc::alloc::Global" ] ]
          ]
          (* Instance *) [ ("from", InstanceField.Method (from T)) ].
    End Impl_core_convert_From_where_core_clone_Clone_T_ref__alloc_vec_Vec_T_alloc_alloc_Global_for_alloc_borrow_Cow_slice_T.
    
    Module Impl_core_iter_traits_collect_FromIterator_where_core_clone_Clone_T_T_for_alloc_borrow_Cow_slice_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::borrow::Cow") [] [ Ty.apply (Ty.path "slice") [] [ T ] ].
      
      (*
          fn from_iter<I: IntoIterator<Item = T>>(it: I) -> Cow<'a, [T]> {
              Cow::Owned(FromIterator::from_iter(it))
          }
      *)
      Definition from_iter (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [ _ as I ], [ it ] =>
          ltac:(M.monadic
            (let it := M.alloc (| it |) in
            Value.StructTuple
              "alloc::borrow::Cow::Owned"
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::iter::traits::collect::FromIterator",
                    Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; Ty.path "alloc::alloc::Global" ],
                    [ T ],
                    "from_iter",
                    [ I ]
                  |),
                  [ M.read (| it |) ]
                |)
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::collect::FromIterator"
          (Self T)
          (* Trait polymorphic types *) [ (* A *) T ]
          (* Instance *) [ ("from_iter", InstanceField.Method (from_iter T)) ].
    End Impl_core_iter_traits_collect_FromIterator_where_core_clone_Clone_T_T_for_alloc_borrow_Cow_slice_T.
  End cow.
End vec.
