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

Module error.
  (* Trait *)
  Module Error.
    Definition source (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.StructTuple "core::option::Option::None" []))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom ProvidedMethod_source : M.IsProvidedMethod "core::error::Error" "source" source.
    Definition type_id (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; β1 ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let β1 := M.alloc (| β1 |) in
          M.match_operator (|
            β1,
            [
              fun γ =>
                ltac:(M.monadic
                  (M.call_closure (|
                    M.get_associated_function (| Ty.path "core::any::TypeId", "of", [ Self ] |),
                    []
                  |)))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom ProvidedMethod_type_id : M.IsProvidedMethod "core::error::Error" "type_id" type_id.
    Definition description
        (Self : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (| Value.String "description() is deprecated; use Display" |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom ProvidedMethod_description :
      M.IsProvidedMethod "core::error::Error" "description" description.
    Definition cause (Self : Ty.t) (ε : 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::error::Error", Self, [], "source", [] |),
            [ M.read (| self |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom ProvidedMethod_cause : M.IsProvidedMethod "core::error::Error" "cause" cause.
    Definition provide (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; request ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let request := M.alloc (| request |) in
          Value.Tuple []))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom ProvidedMethod_provide : M.IsProvidedMethod "core::error::Error" "provide" provide.
  End Error.
  
  Module private.
    (* StructTuple
      {
        name := "Internal";
        const_params := [];
        ty_params := [];
        fields := [];
      } *)
    
    Module Impl_core_fmt_Debug_for_core_error_private_Internal.
      Definition Self : Ty.t := Ty.path "core::error::private::Internal".
      
      (*     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", "write_str", [] |),
              [ M.read (| f |); M.read (| Value.String "Internal" |) ]
            |)))
        | _, _, _ => 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_core_error_private_Internal.
  End private.
  
  Module Impl_core_error_Error_for_never.
    Definition Self : Ty.t := Ty.path "never".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::error::Error"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_error_Error_for_never.
  
  Module Impl_Dyn_core_error_Error_Trait.
    Definition Self : Ty.t := Ty.dyn [ ("core::error::Error::Trait", []) ].
    
    (*
        pub fn is<T: Error + 'static>(&self) -> bool {
            // Get `TypeId` of the type this function is instantiated with.
            let t = TypeId::of::<T>();
    
            // Get `TypeId` of the type in the trait object (`self`).
            let concrete = self.type_id(private::Internal);
    
            // Compare both `TypeId`s on equality.
            t == concrete
        }
    *)
    Definition is (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            let~ t :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "core::any::TypeId", "of", [ T ] |),
                  []
                |)
              |) in
            let~ concrete :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::error::Error",
                    Ty.dyn [ ("core::error::Error::Trait", []) ],
                    [],
                    "type_id",
                    []
                  |),
                  [ M.read (| self |); Value.StructTuple "core::error::private::Internal" [] ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::cmp::PartialEq",
                  Ty.path "core::any::TypeId",
                  [ Ty.path "core::any::TypeId" ],
                  "eq",
                  []
                |),
                [ t; concrete ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is : M.IsAssociatedFunction Self "is" is.
    
    (*
        pub fn downcast_ref<T: Error + 'static>(&self) -> Option<&T> {
            if self.is::<T>() {
                // SAFETY: `is` ensures this type cast is correct
                unsafe { Some(&*(self as *const dyn Error as *const T)) }
            } else {
                None
            }
        }
    *)
    Definition downcast_ref (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.dyn [ ("core::error::Error::Trait", []) ],
                              "is",
                              [ T ]
                            |),
                            [ M.read (| self |) ]
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::option::Option::Some"
                        [ M.rust_cast (M.read (| M.use (M.alloc (| M.read (| self |) |)) |)) ]
                    |)));
                fun γ =>
                  ltac:(M.monadic (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_downcast_ref : M.IsAssociatedFunction Self "downcast_ref" downcast_ref.
    
    (*
        pub fn downcast_mut<T: Error + 'static>(&mut self) -> Option<&mut T> {
            if self.is::<T>() {
                // SAFETY: `is` ensures this type cast is correct
                unsafe { Some(&mut *(self as *mut dyn Error as *mut T)) }
            } else {
                None
            }
        }
    *)
    Definition downcast_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.dyn [ ("core::error::Error::Trait", []) ],
                              "is",
                              [ T ]
                            |),
                            [ M.read (| self |) ]
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::option::Option::Some"
                        [ M.rust_cast (M.read (| M.use (M.alloc (| M.read (| self |) |)) |)) ]
                    |)));
                fun γ =>
                  ltac:(M.monadic (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_downcast_mut : M.IsAssociatedFunction Self "downcast_mut" downcast_mut.
    (*
        pub fn sources(&self) -> Source<'_> {
            // You may think this method would be better in the Error trait, and you'd be right.
            // Unfortunately that doesn't work, not because of the object safety rules but because we
            // save a reference to self in Sources below as a trait object. If this method was
            // declared in Error, then self would have the type &T where T is some concrete type which
            // implements Error. We would need to coerce self to have type &dyn Error, but that requires
            // that Self has a known size (i.e., Self: Sized). We can't put that bound on Error
            // since that would forbid Error trait objects, and we can't put that bound on the method
            // because that means the method can't be called on trait objects (we'd also need the
            // 'static bound, but that isn't allowed because methods with bounds on Self other than
            // Sized are not object-safe). Requiring an Unsize bound is not backwards compatible.
    
            Source { current: Some(self) }
        }
    *)
    Definition sources (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.StructRecord
            "core::error::Source"
            [ ("current", Value.StructTuple "core::option::Option::Some" [ M.read (| self |) ]) ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_sources : M.IsAssociatedFunction Self "sources" sources.
  End Impl_Dyn_core_error_Error_Trait.
  
  Module Impl_Dyn_core_error_Error_Trait_core_marker_Send_AutoTrait.
    Definition Self : Ty.t :=
      Ty.dyn [ ("core::error::Error::Trait", []); ("core::marker::Send::AutoTrait", []) ].
    
    (*
        pub fn is<T: Error + 'static>(&self) -> bool {
            <dyn Error + 'static>::is::<T>(self)
        }
    *)
    Definition is (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.dyn [ ("core::error::Error::Trait", []) ],
              "is",
              [ T ]
            |),
            [ M.read (| self |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is : M.IsAssociatedFunction Self "is" is.
    
    (*
        pub fn downcast_ref<T: Error + 'static>(&self) -> Option<&T> {
            <dyn Error + 'static>::downcast_ref::<T>(self)
        }
    *)
    Definition downcast_ref (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.dyn [ ("core::error::Error::Trait", []) ],
              "downcast_ref",
              [ T ]
            |),
            [ M.read (| self |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_downcast_ref : M.IsAssociatedFunction Self "downcast_ref" downcast_ref.
    
    (*
        pub fn downcast_mut<T: Error + 'static>(&mut self) -> Option<&mut T> {
            <dyn Error + 'static>::downcast_mut::<T>(self)
        }
    *)
    Definition downcast_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.dyn [ ("core::error::Error::Trait", []) ],
              "downcast_mut",
              [ T ]
            |),
            [ M.read (| self |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_downcast_mut : M.IsAssociatedFunction Self "downcast_mut" downcast_mut.
  End Impl_Dyn_core_error_Error_Trait_core_marker_Send_AutoTrait.
  
  Module Impl_Dyn_core_error_Error_Trait_core_marker_Send_AutoTrait_core_marker_Sync_AutoTrait.
    Definition Self : Ty.t :=
      Ty.dyn
        [
          ("core::error::Error::Trait", []);
          ("core::marker::Send::AutoTrait", []);
          ("core::marker::Sync::AutoTrait", [])
        ].
    
    (*
        pub fn is<T: Error + 'static>(&self) -> bool {
            <dyn Error + 'static>::is::<T>(self)
        }
    *)
    Definition is (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.dyn [ ("core::error::Error::Trait", []) ],
              "is",
              [ T ]
            |),
            [ M.read (| self |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is : M.IsAssociatedFunction Self "is" is.
    
    (*
        pub fn downcast_ref<T: Error + 'static>(&self) -> Option<&T> {
            <dyn Error + 'static>::downcast_ref::<T>(self)
        }
    *)
    Definition downcast_ref (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.dyn [ ("core::error::Error::Trait", []) ],
              "downcast_ref",
              [ T ]
            |),
            [ M.read (| self |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_downcast_ref : M.IsAssociatedFunction Self "downcast_ref" downcast_ref.
    
    (*
        pub fn downcast_mut<T: Error + 'static>(&mut self) -> Option<&mut T> {
            <dyn Error + 'static>::downcast_mut::<T>(self)
        }
    *)
    Definition downcast_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.dyn [ ("core::error::Error::Trait", []) ],
              "downcast_mut",
              [ T ]
            |),
            [ M.read (| self |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_downcast_mut : M.IsAssociatedFunction Self "downcast_mut" downcast_mut.
  End Impl_Dyn_core_error_Error_Trait_core_marker_Send_AutoTrait_core_marker_Sync_AutoTrait.
  
  
  (*
  pub fn request_value<'a, T>(err: &'a (impl Error + ?Sized)) -> Option<T>
  where
      T: 'static,
  {
      request_by_type_tag::<'a, tags::Value<T>>(err)
  }
  *)
  Definition request_value (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T; impl_Error__plus___Sized ], [ err ] =>
      ltac:(M.monadic
        (let err := M.alloc (| err |) in
        M.call_closure (|
          M.get_function (|
            "core::error::request_by_type_tag",
            [ Ty.apply (Ty.path "core::error::tags::Value") [] [ T ]; impl_Error__plus___Sized ]
          |),
          [ M.read (| err |) ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_request_value : M.IsFunction "core::error::request_value" request_value.
  
  (*
  pub fn request_ref<'a, T>(err: &'a (impl Error + ?Sized)) -> Option<&'a T>
  where
      T: 'static + ?Sized,
  {
      request_by_type_tag::<'a, tags::Ref<tags::MaybeSizedValue<T>>>(err)
  }
  *)
  Definition request_ref (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T; impl_Error__plus___Sized ], [ err ] =>
      ltac:(M.monadic
        (let err := M.alloc (| err |) in
        M.call_closure (|
          M.get_function (|
            "core::error::request_by_type_tag",
            [
              Ty.apply
                (Ty.path "core::error::tags::Ref")
                []
                [ Ty.apply (Ty.path "core::error::tags::MaybeSizedValue") [] [ T ] ];
              impl_Error__plus___Sized
            ]
          |),
          [ M.read (| err |) ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_request_ref : M.IsFunction "core::error::request_ref" request_ref.
  
  (*
  fn request_by_type_tag<'a, I>(err: &'a (impl Error + ?Sized)) -> Option<I::Reified>
  where
      I: tags::Type<'a>,
  {
      let mut tagged = Tagged { tag_id: TypeId::of::<I>(), value: TaggedOption::<'a, I>(None) };
      err.provide(tagged.as_request());
      tagged.value.0
  }
  *)
  Definition request_by_type_tag (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ _ as I; impl_Error__plus___Sized ], [ err ] =>
      ltac:(M.monadic
        (let err := M.alloc (| err |) in
        M.read (|
          let~ tagged :=
            M.alloc (|
              Value.StructRecord
                "core::error::Tagged"
                [
                  ("tag_id",
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "core::any::TypeId", "of", [ I ] |),
                      []
                    |));
                  ("value",
                    Value.StructTuple
                      "core::error::TaggedOption"
                      [ Value.StructTuple "core::option::Option::None" [] ])
                ]
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::error::Error",
                  impl_Error__plus___Sized,
                  [],
                  "provide",
                  []
                |),
                [
                  M.read (| err |);
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "core::error::Tagged")
                        []
                        [ Ty.apply (Ty.path "core::error::TaggedOption") [] [ I ] ],
                      "as_request",
                      []
                    |),
                    [ tagged ]
                  |)
                ]
              |)
            |) in
          M.SubPointer.get_struct_tuple_field (|
            M.SubPointer.get_struct_record_field (| tagged, "core::error::Tagged", "value" |),
            "core::error::TaggedOption",
            0
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_request_by_type_tag :
    M.IsFunction "core::error::request_by_type_tag" request_by_type_tag.
  
  (* StructTuple
    {
      name := "Request";
      const_params := [];
      ty_params := [];
      fields :=
        [
          Ty.apply
            (Ty.path "core::error::Tagged")
            []
            [ Ty.dyn [ ("core::error::Erased::Trait", []) ] ]
        ];
    } *)
  
  Module Impl_core_error_Request.
    Definition Self : Ty.t := Ty.path "core::error::Request".
    
    (*
        pub fn provide_value<T>(&mut self, value: T) -> &mut Self
        where
            T: 'static,
        {
            self.provide::<tags::Value<T>>(value)
        }
    *)
    Definition provide_value (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ self; value ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let value := M.alloc (| value |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "core::error::Request",
              "provide",
              [ Ty.apply (Ty.path "core::error::tags::Value") [] [ T ] ]
            |),
            [ M.read (| self |); M.read (| value |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_provide_value :
      M.IsAssociatedFunction Self "provide_value" provide_value.
    
    (*
        pub fn provide_value_with<T>(&mut self, fulfil: impl FnOnce() -> T) -> &mut Self
        where
            T: 'static,
        {
            self.provide_with::<tags::Value<T>>(fulfil)
        }
    *)
    Definition provide_value_with (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T; impl_FnOnce___arrow_T ], [ self; fulfil ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let fulfil := M.alloc (| fulfil |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "core::error::Request",
              "provide_with",
              [ Ty.apply (Ty.path "core::error::tags::Value") [] [ T ]; impl_FnOnce___arrow_T ]
            |),
            [ M.read (| self |); M.read (| fulfil |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_provide_value_with :
      M.IsAssociatedFunction Self "provide_value_with" provide_value_with.
    
    (*
        pub fn provide_ref<T: ?Sized + 'static>(&mut self, value: &'a T) -> &mut Self {
            self.provide::<tags::Ref<tags::MaybeSizedValue<T>>>(value)
        }
    *)
    Definition provide_ref (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ self; value ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let value := M.alloc (| value |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "core::error::Request",
              "provide",
              [
                Ty.apply
                  (Ty.path "core::error::tags::Ref")
                  []
                  [ Ty.apply (Ty.path "core::error::tags::MaybeSizedValue") [] [ T ] ]
              ]
            |),
            [ M.read (| self |); M.read (| value |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_provide_ref : M.IsAssociatedFunction Self "provide_ref" provide_ref.
    
    (*
        pub fn provide_ref_with<T: ?Sized + 'static>(
            &mut self,
            fulfil: impl FnOnce() -> &'a T,
        ) -> &mut Self {
            self.provide_with::<tags::Ref<tags::MaybeSizedValue<T>>>(fulfil)
        }
    *)
    Definition provide_ref_with (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T; impl_FnOnce___arrow__'a_T ], [ self; fulfil ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let fulfil := M.alloc (| fulfil |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "core::error::Request",
              "provide_with",
              [
                Ty.apply
                  (Ty.path "core::error::tags::Ref")
                  []
                  [ Ty.apply (Ty.path "core::error::tags::MaybeSizedValue") [] [ T ] ];
                impl_FnOnce___arrow__'a_T
              ]
            |),
            [ M.read (| self |); M.read (| fulfil |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_provide_ref_with :
      M.IsAssociatedFunction Self "provide_ref_with" provide_ref_with.
    
    (*
        fn provide<I>(&mut self, value: I::Reified) -> &mut Self
        where
            I: tags::Type<'a>,
        {
            if let Some(res @ TaggedOption(None)) = self.0.downcast_mut::<I>() {
                res.0 = Some(value);
            }
            self
        }
    *)
    Definition provide (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ _ as I ], [ self; value ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let value := M.alloc (| value |) in
          M.read (|
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "core::error::Tagged")
                                []
                                [ Ty.dyn [ ("core::error::Erased::Trait", []) ] ],
                              "downcast_mut",
                              [ I ]
                            |),
                            [
                              M.SubPointer.get_struct_tuple_field (|
                                M.read (| self |),
                                "core::error::Request",
                                0
                              |)
                            ]
                          |)
                        |) in
                      let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::option::Option::Some",
                          0
                        |) in
                      let res := M.copy (| γ0_0 |) in
                      let γ0_0 := M.read (| γ0_0 |) in
                      let γ3_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ0_0,
                          "core::error::TaggedOption",
                          0
                        |) in
                      let _ := M.is_struct_tuple (| γ3_0, "core::option::Option::None" |) in
                      let~ _ :=
                        M.write (|
                          M.SubPointer.get_struct_tuple_field (|
                            M.read (| res |),
                            "core::error::TaggedOption",
                            0
                          |),
                          Value.StructTuple "core::option::Option::Some" [ M.read (| value |) ]
                        |) in
                      M.alloc (| Value.Tuple [] |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            M.alloc (| M.read (| self |) |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_provide : M.IsAssociatedFunction Self "provide" provide.
    
    (*
        fn provide_with<I>(&mut self, fulfil: impl FnOnce() -> I::Reified) -> &mut Self
        where
            I: tags::Type<'a>,
        {
            if let Some(res @ TaggedOption(None)) = self.0.downcast_mut::<I>() {
                res.0 = Some(fulfil());
            }
            self
        }
    *)
    Definition provide_with (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ _ as I; impl_FnOnce___arrow_I_Reified ], [ self; fulfil ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let fulfil := M.alloc (| fulfil |) in
          M.read (|
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "core::error::Tagged")
                                []
                                [ Ty.dyn [ ("core::error::Erased::Trait", []) ] ],
                              "downcast_mut",
                              [ I ]
                            |),
                            [
                              M.SubPointer.get_struct_tuple_field (|
                                M.read (| self |),
                                "core::error::Request",
                                0
                              |)
                            ]
                          |)
                        |) in
                      let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::option::Option::Some",
                          0
                        |) in
                      let res := M.copy (| γ0_0 |) in
                      let γ0_0 := M.read (| γ0_0 |) in
                      let γ3_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ0_0,
                          "core::error::TaggedOption",
                          0
                        |) in
                      let _ := M.is_struct_tuple (| γ3_0, "core::option::Option::None" |) in
                      let~ _ :=
                        M.write (|
                          M.SubPointer.get_struct_tuple_field (|
                            M.read (| res |),
                            "core::error::TaggedOption",
                            0
                          |),
                          Value.StructTuple
                            "core::option::Option::Some"
                            [
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::ops::function::FnOnce",
                                  impl_FnOnce___arrow_I_Reified,
                                  [ Ty.tuple [] ],
                                  "call_once",
                                  []
                                |),
                                [ M.read (| fulfil |); Value.Tuple [] ]
                              |)
                            ]
                        |) in
                      M.alloc (| Value.Tuple [] |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            M.alloc (| M.read (| self |) |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_provide_with : M.IsAssociatedFunction Self "provide_with" provide_with.
    
    (*
        pub fn would_be_satisfied_by_value_of<T>(&self) -> bool
        where
            T: 'static,
        {
            self.would_be_satisfied_by::<tags::Value<T>>()
        }
    *)
    Definition would_be_satisfied_by_value_of
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [ T ], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "core::error::Request",
              "would_be_satisfied_by",
              [ Ty.apply (Ty.path "core::error::tags::Value") [] [ T ] ]
            |),
            [ M.read (| self |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_would_be_satisfied_by_value_of :
      M.IsAssociatedFunction Self "would_be_satisfied_by_value_of" would_be_satisfied_by_value_of.
    
    (*
        pub fn would_be_satisfied_by_ref_of<T>(&self) -> bool
        where
            T: ?Sized + 'static,
        {
            self.would_be_satisfied_by::<tags::Ref<tags::MaybeSizedValue<T>>>()
        }
    *)
    Definition would_be_satisfied_by_ref_of
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [ T ], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "core::error::Request",
              "would_be_satisfied_by",
              [
                Ty.apply
                  (Ty.path "core::error::tags::Ref")
                  []
                  [ Ty.apply (Ty.path "core::error::tags::MaybeSizedValue") [] [ T ] ]
              ]
            |),
            [ M.read (| self |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_would_be_satisfied_by_ref_of :
      M.IsAssociatedFunction Self "would_be_satisfied_by_ref_of" would_be_satisfied_by_ref_of.
    
    (*
        fn would_be_satisfied_by<I>(&self) -> bool
        where
            I: tags::Type<'a>,
        {
            matches!(self.0.downcast::<I>(), Some(TaggedOption(None)))
        }
    *)
    Definition would_be_satisfied_by (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ _ as I ], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "core::error::Tagged")
                      []
                      [ Ty.dyn [ ("core::error::Erased::Trait", []) ] ],
                    "downcast",
                    [ I ]
                  |),
                  [
                    M.SubPointer.get_struct_tuple_field (|
                      M.read (| self |),
                      "core::error::Request",
                      0
                    |)
                  ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let γ0_0 := M.read (| γ0_0 |) in
                    let γ2_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ0_0,
                        "core::error::TaggedOption",
                        0
                      |) in
                    let _ := M.is_struct_tuple (| γ2_0, "core::option::Option::None" |) in
                    M.alloc (| Value.Bool true |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_would_be_satisfied_by :
      M.IsAssociatedFunction Self "would_be_satisfied_by" would_be_satisfied_by.
  End Impl_core_error_Request.
  
  Module Impl_core_fmt_Debug_for_core_error_Request.
    Definition Self : Ty.t := Ty.path "core::error::Request".
    
    (*
        fn fmt(&self, f: &mut Formatter<'_>) -> Result {
            f.debug_struct("Request").finish_non_exhaustive()
        }
    *)
    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::builders::DebugStruct",
              "finish_non_exhaustive",
              []
            |),
            [
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "core::fmt::Formatter",
                    "debug_struct",
                    []
                  |),
                  [ M.read (| f |); M.read (| Value.String "Request" |) ]
                |)
              |)
            ]
          |)))
      | _, _, _ => 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_core_error_Request.
  
  Module tags.
    (* Trait *)
    (* Empty module 'Type_' *)
    
    (* Trait *)
    (* Empty module 'MaybeSizedType' *)
    
    Module Impl_core_error_tags_MaybeSizedType_where_core_error_tags_Type_T_for_T.
      Definition Self (T : Ty.t) : Ty.t := T.
      
      (*         type Reified = T::Reified; *)
      Definition _Reified (T : Ty.t) : Ty.t := Ty.associated.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::error::tags::MaybeSizedType"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("Reified", InstanceField.Ty (_Reified T)) ].
    End Impl_core_error_tags_MaybeSizedType_where_core_error_tags_Type_T_for_T.
    
    (* StructTuple
      {
        name := "Value";
        const_params := [];
        ty_params := [ "T" ];
        fields := [ Ty.apply (Ty.path "core::marker::PhantomData") [] [ T ] ];
      } *)
    
    Module Impl_core_fmt_Debug_where_core_fmt_Debug_T_for_core_error_tags_Value_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::error::tags::Value") [] [ T ].
      
      (*     Debug *)
      Definition fmt (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T 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_associated_function (|
                Ty.path "core::fmt::Formatter",
                "debug_tuple_field1_finish",
                []
              |),
              [
                M.read (| f |);
                M.read (| Value.String "Value" |);
                M.alloc (|
                  M.SubPointer.get_struct_tuple_field (|
                    M.read (| self |),
                    "core::error::tags::Value",
                    0
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::fmt::Debug"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method (fmt T)) ].
    End Impl_core_fmt_Debug_where_core_fmt_Debug_T_for_core_error_tags_Value_T.
    
    Module Impl_core_error_tags_Type_for_core_error_tags_Value_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::error::tags::Value") [] [ T ].
      
      (*         type Reified = T; *)
      Definition _Reified (T : Ty.t) : Ty.t := T.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::error::tags::Type"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("Reified", InstanceField.Ty (_Reified T)) ].
    End Impl_core_error_tags_Type_for_core_error_tags_Value_T.
    
    (* StructTuple
      {
        name := "MaybeSizedValue";
        const_params := [];
        ty_params := [ "T" ];
        fields := [ Ty.apply (Ty.path "core::marker::PhantomData") [] [ T ] ];
      } *)
    
    Module Impl_core_fmt_Debug_where_core_fmt_Debug_T_where_core_marker_Sized_T_for_core_error_tags_MaybeSizedValue_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::error::tags::MaybeSizedValue") [] [ T ].
      
      (*     Debug *)
      Definition fmt (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T 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_associated_function (|
                Ty.path "core::fmt::Formatter",
                "debug_tuple_field1_finish",
                []
              |),
              [
                M.read (| f |);
                M.read (| Value.String "MaybeSizedValue" |);
                M.alloc (|
                  M.SubPointer.get_struct_tuple_field (|
                    M.read (| self |),
                    "core::error::tags::MaybeSizedValue",
                    0
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::fmt::Debug"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method (fmt T)) ].
    End Impl_core_fmt_Debug_where_core_fmt_Debug_T_where_core_marker_Sized_T_for_core_error_tags_MaybeSizedValue_T.
    
    Module Impl_core_error_tags_MaybeSizedType_where_core_marker_Sized_T_for_core_error_tags_MaybeSizedValue_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::error::tags::MaybeSizedValue") [] [ T ].
      
      (*         type Reified = T; *)
      Definition _Reified (T : Ty.t) : Ty.t := T.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::error::tags::MaybeSizedType"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("Reified", InstanceField.Ty (_Reified T)) ].
    End Impl_core_error_tags_MaybeSizedType_where_core_marker_Sized_T_for_core_error_tags_MaybeSizedValue_T.
    
    (* StructTuple
      {
        name := "Ref";
        const_params := [];
        ty_params := [ "I" ];
        fields := [ Ty.apply (Ty.path "core::marker::PhantomData") [] [ I ] ];
      } *)
    
    Module Impl_core_fmt_Debug_where_core_fmt_Debug_I_for_core_error_tags_Ref_I.
      Definition Self (I : Ty.t) : Ty.t := Ty.apply (Ty.path "core::error::tags::Ref") [] [ I ].
      
      (*     Debug *)
      Definition fmt (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self I 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_associated_function (|
                Ty.path "core::fmt::Formatter",
                "debug_tuple_field1_finish",
                []
              |),
              [
                M.read (| f |);
                M.read (| Value.String "Ref" |);
                M.alloc (|
                  M.SubPointer.get_struct_tuple_field (|
                    M.read (| self |),
                    "core::error::tags::Ref",
                    0
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (I : Ty.t),
        M.IsTraitInstance
          "core::fmt::Debug"
          (Self I)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method (fmt I)) ].
    End Impl_core_fmt_Debug_where_core_fmt_Debug_I_for_core_error_tags_Ref_I.
    
    Module Impl_core_error_tags_Type_where_core_error_tags_MaybeSizedType_I_for_core_error_tags_Ref_I.
      Definition Self (I : Ty.t) : Ty.t := Ty.apply (Ty.path "core::error::tags::Ref") [] [ I ].
      
      (*         type Reified = &'a I::Reified; *)
      Definition _Reified (I : Ty.t) : Ty.t := Ty.apply (Ty.path "&") [] [ Ty.associated ].
      
      Axiom Implements :
        forall (I : Ty.t),
        M.IsTraitInstance
          "core::error::tags::Type"
          (Self I)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("Reified", InstanceField.Ty (_Reified I)) ].
    End Impl_core_error_tags_Type_where_core_error_tags_MaybeSizedType_I_for_core_error_tags_Ref_I.
  End tags.
  
  (* StructTuple
    {
      name := "TaggedOption";
      const_params := [];
      ty_params := [ "I" ];
      fields := [ Ty.apply (Ty.path "core::option::Option") [] [ Ty.associated ] ];
    } *)
  
  Module Impl_core_error_Tagged_core_error_TaggedOption_I.
    Definition Self (I : Ty.t) : Ty.t :=
      Ty.apply
        (Ty.path "core::error::Tagged")
        []
        [ Ty.apply (Ty.path "core::error::TaggedOption") [] [ I ] ].
    
    (*
        pub(crate) fn as_request(&mut self) -> &mut Request<'a> {
            let erased = self as &mut Tagged<dyn Erased<'a> + 'a>;
            // SAFETY: transmuting `&mut Tagged<dyn Erased<'a> + 'a>` to `&mut Request<'a>` is safe since
            // `Request` is repr(transparent).
            unsafe { &mut *(erased as *mut Tagged<dyn Erased<'a>> as *mut Request<'a>) }
        }
    *)
    Definition as_request (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self I in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            let~ erased := M.copy (| M.use (M.alloc (| M.read (| self |) |)) |) in
            M.alloc (| M.rust_cast (M.read (| M.use (M.alloc (| M.read (| erased |) |)) |)) |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_as_request :
      forall (I : Ty.t),
      M.IsAssociatedFunction (Self I) "as_request" (as_request I).
  End Impl_core_error_Tagged_core_error_TaggedOption_I.
  
  (* Trait *)
  (* Empty module 'Erased' *)
  
  Module Impl_core_error_Erased_where_core_error_tags_Type_I_for_core_error_TaggedOption_I.
    Definition Self (I : Ty.t) : Ty.t := Ty.apply (Ty.path "core::error::TaggedOption") [] [ I ].
    
    Axiom Implements :
      forall (I : Ty.t),
      M.IsTraitInstance
        "core::error::Erased"
        (Self I)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_error_Erased_where_core_error_tags_Type_I_for_core_error_TaggedOption_I.
  
  (* StructRecord
    {
      name := "Tagged";
      const_params := [];
      ty_params := [ "E" ];
      fields := [ ("tag_id", Ty.path "core::any::TypeId"); ("value", E) ];
    } *)
  
  Module Impl_core_error_Tagged_Dyn_core_error_Erased_Trait.
    Definition Self : Ty.t :=
      Ty.apply (Ty.path "core::error::Tagged") [] [ Ty.dyn [ ("core::error::Erased::Trait", []) ] ].
    
    (*
        fn downcast<I>(&self) -> Option<&TaggedOption<'a, I>>
        where
            I: tags::Type<'a>,
        {
            if self.tag_id == TypeId::of::<I>() {
                // SAFETY: Just checked whether we're pointing to an I.
                Some(&unsafe { &*(self as *const Self).cast::<Tagged<TaggedOption<'a, I>>>() }.value)
            } else {
                None
            }
        }
    *)
    Definition downcast (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ _ as I ], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::cmp::PartialEq",
                              Ty.path "core::any::TypeId",
                              [ Ty.path "core::any::TypeId" ],
                              "eq",
                              []
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::error::Tagged",
                                "tag_id"
                              |);
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "core::any::TypeId",
                                    "of",
                                    [ I ]
                                  |),
                                  []
                                |)
                              |)
                            ]
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::option::Option::Some"
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "*const")
                                  []
                                  [
                                    Ty.apply
                                      (Ty.path "core::error::Tagged")
                                      []
                                      [ Ty.dyn [ ("core::error::Erased::Trait", []) ] ]
                                  ],
                                "cast",
                                [
                                  Ty.apply
                                    (Ty.path "core::error::Tagged")
                                    []
                                    [ Ty.apply (Ty.path "core::error::TaggedOption") [] [ I ] ]
                                ]
                              |),
                              [ M.read (| M.use (M.alloc (| M.read (| self |) |)) |) ]
                            |),
                            "core::error::Tagged",
                            "value"
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_downcast : M.IsAssociatedFunction Self "downcast" downcast.
    
    (*
        fn downcast_mut<I>(&mut self) -> Option<&mut TaggedOption<'a, I>>
        where
            I: tags::Type<'a>,
        {
            if self.tag_id == TypeId::of::<I>() {
                Some(
                    // SAFETY: Just checked whether we're pointing to an I.
                    &mut unsafe { &mut *(self as *mut Self).cast::<Tagged<TaggedOption<'a, I>>>() }
                        .value,
                )
            } else {
                None
            }
        }
    *)
    Definition downcast_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ _ as I ], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::cmp::PartialEq",
                              Ty.path "core::any::TypeId",
                              [ Ty.path "core::any::TypeId" ],
                              "eq",
                              []
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::error::Tagged",
                                "tag_id"
                              |);
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "core::any::TypeId",
                                    "of",
                                    [ I ]
                                  |),
                                  []
                                |)
                              |)
                            ]
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::option::Option::Some"
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "*mut")
                                  []
                                  [
                                    Ty.apply
                                      (Ty.path "core::error::Tagged")
                                      []
                                      [ Ty.dyn [ ("core::error::Erased::Trait", []) ] ]
                                  ],
                                "cast",
                                [
                                  Ty.apply
                                    (Ty.path "core::error::Tagged")
                                    []
                                    [ Ty.apply (Ty.path "core::error::TaggedOption") [] [ I ] ]
                                ]
                              |),
                              [ M.read (| M.use (M.alloc (| M.read (| self |) |)) |) ]
                            |),
                            "core::error::Tagged",
                            "value"
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_downcast_mut : M.IsAssociatedFunction Self "downcast_mut" downcast_mut.
  End Impl_core_error_Tagged_Dyn_core_error_Erased_Trait.
  
  (* StructRecord
    {
      name := "Source";
      const_params := [];
      ty_params := [];
      fields :=
        [
          ("current",
            Ty.apply
              (Ty.path "core::option::Option")
              []
              [ Ty.apply (Ty.path "&") [] [ Ty.dyn [ ("core::error::Error::Trait", []) ] ] ])
        ];
    } *)
  
  Module Impl_core_clone_Clone_for_core_error_Source.
    Definition Self : Ty.t := Ty.path "core::error::Source".
    
    (* 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
            "core::error::Source"
            [
              ("current",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [ Ty.apply (Ty.path "&") [] [ Ty.dyn [ ("core::error::Error::Trait", []) ] ]
                      ],
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::error::Source",
                      "current"
                    |)
                  ]
                |))
            ]))
      | _, _, _ => 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_core_error_Source.
  
  Module Impl_core_fmt_Debug_for_core_error_Source.
    Definition Self : Ty.t := Ty.path "core::error::Source".
    
    (* 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 "Source" |);
              M.read (| Value.String "current" |);
              M.alloc (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::error::Source",
                  "current"
                |)
              |)
            ]
          |)))
      | _, _, _ => 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_core_error_Source.
  
  Module Impl_core_iter_traits_iterator_Iterator_for_core_error_Source.
    Definition Self : Ty.t := Ty.path "core::error::Source".
    
    (*     type Item = &'a (dyn Error + 'static); *)
    Definition _Item : Ty.t :=
      Ty.apply (Ty.path "&") [] [ Ty.dyn [ ("core::error::Error::Trait", []) ] ].
    
    (*
        fn next(&mut self) -> Option<Self::Item> {
            let current = self.current;
            self.current = self.current.and_then(Error::source);
            current
        }
    *)
    Definition next (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            let~ current :=
              M.copy (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::error::Source",
                  "current"
                |)
              |) in
            let~ _ :=
              M.write (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::error::Source",
                  "current"
                |),
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [ Ty.apply (Ty.path "&") [] [ Ty.dyn [ ("core::error::Error::Trait", []) ] ]
                      ],
                    "and_then",
                    [
                      Ty.apply (Ty.path "&") [] [ Ty.dyn [ ("core::error::Error::Trait", []) ] ];
                      Ty.function
                        [ Ty.apply (Ty.path "&") [] [ Ty.dyn [ ("core::error::Error::Trait", []) ] ]
                        ]
                        (Ty.apply
                          (Ty.path "core::option::Option")
                          []
                          [
                            Ty.apply
                              (Ty.path "&")
                              []
                              [ Ty.dyn [ ("core::error::Error::Trait", []) ] ]
                          ])
                    ]
                  |),
                  [
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::error::Source",
                        "current"
                      |)
                    |);
                    M.get_trait_method (|
                      "core::error::Error",
                      Ty.dyn [ ("core::error::Error::Trait", []) ],
                      [],
                      "source",
                      []
                    |)
                  ]
                |)
              |) in
            current
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn size_hint(&self) -> (usize, Option<usize>) {
            if self.current.is_some() { (1, None) } else { (0, Some(0)) }
        }
    *)
    Definition size_hint (ε : 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 (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "core::option::Option")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "&")
                                    []
                                    [ Ty.dyn [ ("core::error::Error::Trait", []) ] ]
                                ],
                              "is_some",
                              []
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::error::Source",
                                "current"
                              |)
                            ]
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.Usize 1;
                          Value.StructTuple "core::option::Option::None" []
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.alloc (|
                      Value.Tuple
                        [
                          Value.Integer IntegerKind.Usize 0;
                          Value.StructTuple
                            "core::option::Option::Some"
                            [ Value.Integer IntegerKind.Usize 0 ]
                        ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::iter::traits::iterator::Iterator"
        Self
        (* Trait polymorphic types *) []
        (* Instance *)
        [
          ("Item", InstanceField.Ty _Item);
          ("next", InstanceField.Method next);
          ("size_hint", InstanceField.Method size_hint)
        ].
  End Impl_core_iter_traits_iterator_Iterator_for_core_error_Source.
  
  Module Impl_core_iter_traits_marker_FusedIterator_for_core_error_Source.
    Definition Self : Ty.t := Ty.path "core::error::Source".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::iter::traits::marker::FusedIterator"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_iter_traits_marker_FusedIterator_for_core_error_Source.
  
  Module Impl_core_error_Error_where_core_error_Error_T_where_core_marker_Sized_T_for_ref__T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "&") [] [ T ].
    
    (*
        fn description(&self) -> &str {
            Error::description(&**self)
        }
    *)
    Definition description (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.call_closure (|
            M.get_trait_method (| "core::error::Error", T, [], "description", [] |),
            [ M.read (| M.read (| self |) |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn cause(&self) -> Option<&dyn Error> {
            Error::cause(&**self)
        }
    *)
    Definition cause (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.call_closure (|
            M.get_trait_method (| "core::error::Error", T, [], "cause", [] |),
            [ M.read (| M.read (| self |) |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn source(&self) -> Option<&(dyn Error + 'static)> {
            Error::source(&**self)
        }
    *)
    Definition source (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.call_closure (|
            M.get_trait_method (| "core::error::Error", T, [], "source", [] |),
            [ M.read (| M.read (| self |) |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn provide<'b>(&'b self, request: &mut Request<'b>) {
            Error::provide(&**self, request);
        }
    *)
    Definition provide (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self; request ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let request := M.alloc (| request |) in
          M.read (|
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (| "core::error::Error", T, [], "provide", [] |),
                  [ M.read (| M.read (| self |) |); M.read (| request |) ]
                |)
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::error::Error"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *)
        [
          ("description", InstanceField.Method (description T));
          ("cause", InstanceField.Method (cause T));
          ("source", InstanceField.Method (source T));
          ("provide", InstanceField.Method (provide T))
        ].
  End Impl_core_error_Error_where_core_error_Error_T_where_core_marker_Sized_T_for_ref__T.
  
  Module Impl_core_error_Error_for_core_fmt_Error.
    Definition Self : Ty.t := Ty.path "core::fmt::Error".
    
    (*
        fn description(&self) -> &str {
            "an error occurred when formatting an argument"
        }
    *)
    Definition description (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (| Value.String "an error occurred when formatting an argument" |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::error::Error"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("description", InstanceField.Method description) ].
  End Impl_core_error_Error_for_core_fmt_Error.
  
  Module Impl_core_error_Error_for_core_cell_BorrowError.
    Definition Self : Ty.t := Ty.path "core::cell::BorrowError".
    
    (*
        fn description(&self) -> &str {
            "already mutably borrowed"
        }
    *)
    Definition description (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (| Value.String "already mutably borrowed" |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::error::Error"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("description", InstanceField.Method description) ].
  End Impl_core_error_Error_for_core_cell_BorrowError.
  
  Module Impl_core_error_Error_for_core_cell_BorrowMutError.
    Definition Self : Ty.t := Ty.path "core::cell::BorrowMutError".
    
    (*
        fn description(&self) -> &str {
            "already borrowed"
        }
    *)
    Definition description (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (| Value.String "already borrowed" |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::error::Error"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("description", InstanceField.Method description) ].
  End Impl_core_error_Error_for_core_cell_BorrowMutError.
  
  Module Impl_core_error_Error_for_core_char_convert_CharTryFromError.
    Definition Self : Ty.t := Ty.path "core::char::convert::CharTryFromError".
    
    (*
        fn description(&self) -> &str {
            "converted integer out of range for `char`"
        }
    *)
    Definition description (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (| Value.String "converted integer out of range for `char`" |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::error::Error"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("description", InstanceField.Method description) ].
  End Impl_core_error_Error_for_core_char_convert_CharTryFromError.
  
  Module Impl_core_error_Error_for_core_time_TryFromFloatSecsError.
    Definition Self : Ty.t := Ty.path "core::time::TryFromFloatSecsError".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::error::Error"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_error_Error_for_core_time_TryFromFloatSecsError.
  
  Module Impl_core_error_Error_for_core_ffi_c_str_FromBytesUntilNulError.
    Definition Self : Ty.t := Ty.path "core::ffi::c_str::FromBytesUntilNulError".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::error::Error"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_error_Error_for_core_ffi_c_str_FromBytesUntilNulError.
  
  Module Impl_core_error_Error_for_core_slice_GetManyMutError_N.
    Definition Self (N : Value.t) : Ty.t :=
      Ty.apply (Ty.path "core::slice::GetManyMutError") [ N ] [].
    
    Axiom Implements :
      forall (N : Value.t),
      M.IsTraitInstance
        "core::error::Error"
        (Self N)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_error_Error_for_core_slice_GetManyMutError_N.
End error.
