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

Module collections.
  (* StructRecord
    {
      name := "TryReserveError";
      const_params := [];
      ty_params := [];
      fields := [ ("kind", Ty.path "alloc::collections::TryReserveErrorKind") ];
    } *)
  
  Module Impl_core_clone_Clone_for_alloc_collections_TryReserveError.
    Definition Self : Ty.t := Ty.path "alloc::collections::TryReserveError".
    
    (* Clone *)
    Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.StructRecord
            "alloc::collections::TryReserveError"
            [
              ("kind",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.path "alloc::collections::TryReserveErrorKind",
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "alloc::collections::TryReserveError",
                      "kind"
                    |)
                  ]
                |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::clone::Clone"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("clone", InstanceField.Method clone) ].
  End Impl_core_clone_Clone_for_alloc_collections_TryReserveError.
  
  Module Impl_core_marker_StructuralPartialEq_for_alloc_collections_TryReserveError.
    Definition Self : Ty.t := Ty.path "alloc::collections::TryReserveError".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_alloc_collections_TryReserveError.
  
  Module Impl_core_cmp_PartialEq_for_alloc_collections_TryReserveError.
    Definition Self : Ty.t := Ty.path "alloc::collections::TryReserveError".
    
    (* PartialEq *)
    Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      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.path "alloc::collections::TryReserveErrorKind",
              [ Ty.path "alloc::collections::TryReserveErrorKind" ],
              "eq",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "alloc::collections::TryReserveError",
                "kind"
              |);
              M.SubPointer.get_struct_record_field (|
                M.read (| other |),
                "alloc::collections::TryReserveError",
                "kind"
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::PartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("eq", InstanceField.Method eq) ].
  End Impl_core_cmp_PartialEq_for_alloc_collections_TryReserveError.
  
  Module Impl_core_cmp_Eq_for_alloc_collections_TryReserveError.
    Definition Self : Ty.t := Ty.path "alloc::collections::TryReserveError".
    
    (* Eq *)
    Definition assert_receiver_is_total_eq
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              Value.DeclaredButUndefined,
              [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::Eq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *)
        [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
  End Impl_core_cmp_Eq_for_alloc_collections_TryReserveError.
  
  Module Impl_core_fmt_Debug_for_alloc_collections_TryReserveError.
    Definition Self : Ty.t := Ty.path "alloc::collections::TryReserveError".
    
    (* Debug *)
    Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "core::fmt::Formatter",
              "debug_struct_field1_finish",
              []
            |),
            [
              M.read (| f |);
              M.read (| Value.String "TryReserveError" |);
              M.read (| Value.String "kind" |);
              M.alloc (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "alloc::collections::TryReserveError",
                  "kind"
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::fmt::Debug"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
  End Impl_core_fmt_Debug_for_alloc_collections_TryReserveError.
  
  Module Impl_alloc_collections_TryReserveError.
    Definition Self : Ty.t := Ty.path "alloc::collections::TryReserveError".
    
    (*
        pub fn kind(&self) -> TryReserveErrorKind {
            self.kind.clone()
        }
    *)
    Definition kind (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::clone::Clone",
              Ty.path "alloc::collections::TryReserveErrorKind",
              [],
              "clone",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "alloc::collections::TryReserveError",
                "kind"
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_kind : M.IsAssociatedFunction Self "kind" kind.
  End Impl_alloc_collections_TryReserveError.
  
  (*
  Enum TryReserveErrorKind
  {
    const_params := [];
    ty_params := [];
    variants :=
      [
        {
          name := "CapacityOverflow";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "AllocError";
          item :=
            StructRecord
              [ ("layout", Ty.path "core::alloc::layout::Layout"); ("non_exhaustive", Ty.tuple [])
              ];
          discriminant := None;
        }
      ];
  }
  *)
  
  Module Impl_core_clone_Clone_for_alloc_collections_TryReserveErrorKind.
    Definition Self : Ty.t := Ty.path "alloc::collections::TryReserveErrorKind".
    
    (* Clone *)
    Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "alloc::collections::TryReserveErrorKind::CapacityOverflow"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "alloc::collections::TryReserveErrorKind::CapacityOverflow"
                        []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "alloc::collections::TryReserveErrorKind::AllocError",
                        "layout"
                      |) in
                    let γ1_1 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "alloc::collections::TryReserveErrorKind::AllocError",
                        "non_exhaustive"
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    let __self_1 := M.alloc (| γ1_1 |) in
                    M.alloc (|
                      Value.StructRecord
                        "alloc::collections::TryReserveErrorKind::AllocError"
                        [
                          ("layout",
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::clone::Clone",
                                Ty.path "core::alloc::layout::Layout",
                                [],
                                "clone",
                                []
                              |),
                              [ M.read (| __self_0 |) ]
                            |));
                          ("non_exhaustive",
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::clone::Clone",
                                Ty.tuple [],
                                [],
                                "clone",
                                []
                              |),
                              [ M.read (| __self_1 |) ]
                            |))
                        ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::clone::Clone"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("clone", InstanceField.Method clone) ].
  End Impl_core_clone_Clone_for_alloc_collections_TryReserveErrorKind.
  
  Module Impl_core_marker_StructuralPartialEq_for_alloc_collections_TryReserveErrorKind.
    Definition Self : Ty.t := Ty.path "alloc::collections::TryReserveErrorKind".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_alloc_collections_TryReserveErrorKind.
  
  Module Impl_core_cmp_PartialEq_for_alloc_collections_TryReserveErrorKind.
    Definition Self : Ty.t := Ty.path "alloc::collections::TryReserveErrorKind".
    
    (* PartialEq *)
    Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.read (|
            let~ __self_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "alloc::collections::TryReserveErrorKind" ]
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            let~ __arg1_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "alloc::collections::TryReserveErrorKind" ]
                  |),
                  [ M.read (| other |) ]
                |)
              |) in
            M.alloc (|
              LogicalOp.and (|
                BinOp.eq (| M.read (| __self_discr |), M.read (| __arg1_discr |) |),
                ltac:(M.monadic
                  (M.read (|
                    M.match_operator (|
                      M.alloc (| Value.Tuple [ M.read (| self |); M.read (| other |) ] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                            let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                            let γ0_0 := M.read (| γ0_0 |) in
                            let γ2_0 :=
                              M.SubPointer.get_struct_record_field (|
                                γ0_0,
                                "alloc::collections::TryReserveErrorKind::AllocError",
                                "layout"
                              |) in
                            let γ2_1 :=
                              M.SubPointer.get_struct_record_field (|
                                γ0_0,
                                "alloc::collections::TryReserveErrorKind::AllocError",
                                "non_exhaustive"
                              |) in
                            let __self_0 := M.alloc (| γ2_0 |) in
                            let __self_1 := M.alloc (| γ2_1 |) in
                            let γ0_1 := M.read (| γ0_1 |) in
                            let γ2_0 :=
                              M.SubPointer.get_struct_record_field (|
                                γ0_1,
                                "alloc::collections::TryReserveErrorKind::AllocError",
                                "layout"
                              |) in
                            let γ2_1 :=
                              M.SubPointer.get_struct_record_field (|
                                γ0_1,
                                "alloc::collections::TryReserveErrorKind::AllocError",
                                "non_exhaustive"
                              |) in
                            let __arg1_0 := M.alloc (| γ2_0 |) in
                            let __arg1_1 := M.alloc (| γ2_1 |) in
                            M.alloc (|
                              LogicalOp.and (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::cmp::PartialEq",
                                    Ty.apply
                                      (Ty.path "&")
                                      []
                                      [ Ty.path "core::alloc::layout::Layout" ],
                                    [
                                      Ty.apply
                                        (Ty.path "&")
                                        []
                                        [ Ty.path "core::alloc::layout::Layout" ]
                                    ],
                                    "eq",
                                    []
                                  |),
                                  [ __self_0; __arg1_0 ]
                                |),
                                ltac:(M.monadic
                                  (M.call_closure (|
                                    M.get_trait_method (|
                                      "core::cmp::PartialEq",
                                      Ty.apply (Ty.path "&") [] [ Ty.tuple [] ],
                                      [ Ty.apply (Ty.path "&") [] [ Ty.tuple [] ] ],
                                      "eq",
                                      []
                                    |),
                                    [ __self_1; __arg1_1 ]
                                  |)))
                              |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Bool true |)))
                      ]
                    |)
                  |)))
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::PartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("eq", InstanceField.Method eq) ].
  End Impl_core_cmp_PartialEq_for_alloc_collections_TryReserveErrorKind.
  
  Module Impl_core_cmp_Eq_for_alloc_collections_TryReserveErrorKind.
    Definition Self : Ty.t := Ty.path "alloc::collections::TryReserveErrorKind".
    
    (* Eq *)
    Definition assert_receiver_is_total_eq
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              Value.DeclaredButUndefined,
              [
                fun γ =>
                  ltac:(M.monadic
                    (M.match_operator (|
                      Value.DeclaredButUndefined,
                      [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::Eq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *)
        [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
  End Impl_core_cmp_Eq_for_alloc_collections_TryReserveErrorKind.
  
  Module Impl_core_fmt_Debug_for_alloc_collections_TryReserveErrorKind.
    Definition Self : Ty.t := Ty.path "alloc::collections::TryReserveErrorKind".
    
    (* Debug *)
    Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "alloc::collections::TryReserveErrorKind::CapacityOverflow"
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_str",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "CapacityOverflow" |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "alloc::collections::TryReserveErrorKind::AllocError",
                        "layout"
                      |) in
                    let γ1_1 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "alloc::collections::TryReserveErrorKind::AllocError",
                        "non_exhaustive"
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    let __self_1 := M.alloc (| γ1_1 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "debug_struct_field2_finish",
                          []
                        |),
                        [
                          M.read (| f |);
                          M.read (| Value.String "AllocError" |);
                          M.read (| Value.String "layout" |);
                          M.read (| __self_0 |);
                          M.read (| Value.String "non_exhaustive" |);
                          __self_1
                        ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::fmt::Debug"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
  End Impl_core_fmt_Debug_for_alloc_collections_TryReserveErrorKind.
  
  Module Impl_core_convert_From_alloc_collections_TryReserveErrorKind_for_alloc_collections_TryReserveError.
    Definition Self : Ty.t := Ty.path "alloc::collections::TryReserveError".
    
    (*
        fn from(kind: TryReserveErrorKind) -> Self {
            Self { kind }
        }
    *)
    Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ kind ] =>
        ltac:(M.monadic
          (let kind := M.alloc (| kind |) in
          Value.StructRecord "alloc::collections::TryReserveError" [ ("kind", M.read (| kind |)) ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::convert::From"
        Self
        (* Trait polymorphic types *) [ (* T *) Ty.path "alloc::collections::TryReserveErrorKind" ]
        (* Instance *) [ ("from", InstanceField.Method from) ].
  End Impl_core_convert_From_alloc_collections_TryReserveErrorKind_for_alloc_collections_TryReserveError.
  
  Module Impl_core_convert_From_core_alloc_layout_LayoutError_for_alloc_collections_TryReserveErrorKind.
    Definition Self : Ty.t := Ty.path "alloc::collections::TryReserveErrorKind".
    
    (*
        fn from(_: LayoutError) -> Self {
            TryReserveErrorKind::CapacityOverflow
        }
    *)
    Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ β0 ] =>
        ltac:(M.monadic
          (let β0 := M.alloc (| β0 |) in
          M.match_operator (|
            β0,
            [
              fun γ =>
                ltac:(M.monadic
                  (Value.StructTuple
                    "alloc::collections::TryReserveErrorKind::CapacityOverflow"
                    []))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::convert::From"
        Self
        (* Trait polymorphic types *) [ (* T *) Ty.path "core::alloc::layout::LayoutError" ]
        (* Instance *) [ ("from", InstanceField.Method from) ].
  End Impl_core_convert_From_core_alloc_layout_LayoutError_for_alloc_collections_TryReserveErrorKind.
  
  Module Impl_core_fmt_Display_for_alloc_collections_TryReserveError.
    Definition Self : Ty.t := Ty.path "alloc::collections::TryReserveError".
    
    (*
        fn fmt(
            &self,
            fmt: &mut core::fmt::Formatter<'_>,
        ) -> core::result::Result<(), core::fmt::Error> {
            fmt.write_str("memory allocation failed")?;
            let reason = match self.kind {
                TryReserveErrorKind::CapacityOverflow => {
                    " because the computed capacity exceeded the collection's maximum"
                }
                TryReserveErrorKind::AllocError { .. } => {
                    " because the memory allocator returned an error"
                }
            };
            fmt.write_str(reason)
        }
    *)
    Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; fmt ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let fmt := M.alloc (| fmt |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::try_trait::Try",
                          Ty.apply
                            (Ty.path "core::result::Result")
                            []
                            [ Ty.tuple []; Ty.path "core::fmt::Error" ],
                          [],
                          "branch",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Formatter",
                              "write_str",
                              []
                            |),
                            [ M.read (| fmt |); M.read (| Value.String "memory allocation failed" |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "core::ops::control_flow::ControlFlow::Break",
                              0
                            |) in
                          let residual := M.copy (| γ0_0 |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                M.return_ (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::ops::try_trait::FromResidual",
                                      Ty.apply
                                        (Ty.path "core::result::Result")
                                        []
                                        [ Ty.tuple []; Ty.path "core::fmt::Error" ],
                                      [
                                        Ty.apply
                                          (Ty.path "core::result::Result")
                                          []
                                          [
                                            Ty.path "core::convert::Infallible";
                                            Ty.path "core::fmt::Error"
                                          ]
                                      ],
                                      "from_residual",
                                      []
                                    |),
                                    [ M.read (| residual |) ]
                                  |)
                                |)
                              |)
                            |)
                          |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "core::ops::control_flow::ControlFlow::Continue",
                              0
                            |) in
                          let val := M.copy (| γ0_0 |) in
                          val))
                    ]
                  |) in
                let~ reason :=
                  M.copy (|
                    M.match_operator (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "alloc::collections::TryReserveError",
                        "kind"
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "alloc::collections::TryReserveErrorKind::CapacityOverflow"
                              |) in
                            Value.String
                              " because the computed capacity exceeded the collection's maximum"));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "alloc::collections::TryReserveErrorKind::AllocError"
                              |) in
                            M.alloc (|
                              M.read (|
                                Value.String " because the memory allocator returned an error"
                              |)
                            |)))
                      ]
                    |)
                  |) in
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "core::fmt::Formatter", "write_str", [] |),
                    [ M.read (| fmt |); M.read (| reason |) ]
                  |)
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::fmt::Display"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
  End Impl_core_fmt_Display_for_alloc_collections_TryReserveError.
  
  (* Trait *)
  (* Empty module 'SpecExtend' *)
  
  Module Impl_core_error_Error_for_alloc_collections_TryReserveError.
    Definition Self : Ty.t := Ty.path "alloc::collections::TryReserveError".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::error::Error"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_error_Error_for_alloc_collections_TryReserveError.
End collections.
