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

Module fmt.
  Module rt.
    (* StructRecord
      {
        name := "Placeholder";
        const_params := [];
        ty_params := [];
        fields :=
          [
            ("position", Ty.path "usize");
            ("fill", Ty.path "char");
            ("align", Ty.path "core::fmt::rt::Alignment");
            ("flags", Ty.path "u32");
            ("precision", Ty.path "core::fmt::rt::Count");
            ("width", Ty.path "core::fmt::rt::Count")
          ];
      } *)
    
    Module Impl_core_marker_Copy_for_core_fmt_rt_Placeholder.
      Definition Self : Ty.t := Ty.path "core::fmt::rt::Placeholder".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::Copy"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Copy_for_core_fmt_rt_Placeholder.
    
    Module Impl_core_clone_Clone_for_core_fmt_rt_Placeholder.
      Definition Self : Ty.t := Ty.path "core::fmt::rt::Placeholder".
      
      (* 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 (|
                Value.DeclaredButUndefined,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (M.match_operator (|
                        Value.DeclaredButUndefined,
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (M.match_operator (|
                                Value.DeclaredButUndefined,
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (M.match_operator (|
                                        Value.DeclaredButUndefined,
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (M.match_operator (|
                                                Value.DeclaredButUndefined,
                                                [ fun γ => ltac:(M.monadic (M.read (| self |))) ]
                                              |)))
                                        ]
                                      |)))
                                ]
                              |)))
                        ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => 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_fmt_rt_Placeholder.
    
    Module Impl_core_fmt_rt_Placeholder.
      Definition Self : Ty.t := Ty.path "core::fmt::rt::Placeholder".
      
      (*
          pub const fn new(
              position: usize,
              fill: char,
              align: Alignment,
              flags: u32,
              precision: Count,
              width: Count,
          ) -> Self {
              Self { position, fill, align, flags, precision, width }
          }
      *)
      Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ position; fill; align; flags; precision; width ] =>
          ltac:(M.monadic
            (let position := M.alloc (| position |) in
            let fill := M.alloc (| fill |) in
            let align := M.alloc (| align |) in
            let flags := M.alloc (| flags |) in
            let precision := M.alloc (| precision |) in
            let width := M.alloc (| width |) in
            Value.StructRecord
              "core::fmt::rt::Placeholder"
              [
                ("position", M.read (| position |));
                ("fill", M.read (| fill |));
                ("align", M.read (| align |));
                ("flags", M.read (| flags |));
                ("precision", M.read (| precision |));
                ("width", M.read (| width |))
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
    End Impl_core_fmt_rt_Placeholder.
    
    (*
    Enum Alignment
    {
      const_params := [];
      ty_params := [];
      variants :=
        [
          {
            name := "Left";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "Right";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "Center";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "Unknown";
            item := StructTuple [];
            discriminant := None;
          }
        ];
    }
    *)
    
    Module Impl_core_marker_Copy_for_core_fmt_rt_Alignment.
      Definition Self : Ty.t := Ty.path "core::fmt::rt::Alignment".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::Copy"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Copy_for_core_fmt_rt_Alignment.
    
    Module Impl_core_clone_Clone_for_core_fmt_rt_Alignment.
      Definition Self : Ty.t := Ty.path "core::fmt::rt::Alignment".
      
      (* 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.read (| self |) |)))
        | _, _, _ => 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_fmt_rt_Alignment.
    
    Module Impl_core_marker_StructuralPartialEq_for_core_fmt_rt_Alignment.
      Definition Self : Ty.t := Ty.path "core::fmt::rt::Alignment".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_core_fmt_rt_Alignment.
    
    Module Impl_core_cmp_PartialEq_for_core_fmt_rt_Alignment.
      Definition Self : Ty.t := Ty.path "core::fmt::rt::Alignment".
      
      (* 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 "core::fmt::rt::Alignment" ]
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ __arg1_discr :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::discriminant_value",
                      [ Ty.path "core::fmt::rt::Alignment" ]
                    |),
                    [ M.read (| other |) ]
                  |)
                |) in
              M.alloc (| BinOp.eq (| M.read (| __self_discr |), M.read (| __arg1_discr |) |) |)
            |)))
        | _, _, _ => 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_core_fmt_rt_Alignment.
    
    Module Impl_core_cmp_Eq_for_core_fmt_rt_Alignment.
      Definition Self : Ty.t := Ty.path "core::fmt::rt::Alignment".
      
      (* 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
            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_core_fmt_rt_Alignment.
    
    (*
    Enum Count
    {
      const_params := [];
      ty_params := [];
      variants :=
        [
          {
            name := "Is";
            item := StructTuple [ Ty.path "usize" ];
            discriminant := None;
          };
          {
            name := "Param";
            item := StructTuple [ Ty.path "usize" ];
            discriminant := None;
          };
          {
            name := "Implied";
            item := StructTuple [];
            discriminant := None;
          }
        ];
    }
    *)
    
    Module Impl_core_marker_Copy_for_core_fmt_rt_Count.
      Definition Self : Ty.t := Ty.path "core::fmt::rt::Count".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::Copy"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Copy_for_core_fmt_rt_Count.
    
    Module Impl_core_clone_Clone_for_core_fmt_rt_Count.
      Definition Self : Ty.t := Ty.path "core::fmt::rt::Count".
      
      (* 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 (|
                Value.DeclaredButUndefined,
                [ fun γ => ltac:(M.monadic (M.read (| self |))) ]
              |)
            |)))
        | _, _, _ => 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_fmt_rt_Count.
    
    (*
    Enum Flag
    {
      const_params := [];
      ty_params := [];
      variants :=
        [
          {
            name := "SignPlus";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "SignMinus";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "Alternate";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "SignAwareZeroPad";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "DebugLowerHex";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "DebugUpperHex";
            item := StructTuple [];
            discriminant := None;
          }
        ];
    }
    *)
    
    Module Impl_core_marker_Copy_for_core_fmt_rt_Flag.
      Definition Self : Ty.t := Ty.path "core::fmt::rt::Flag".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::Copy"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Copy_for_core_fmt_rt_Flag.
    
    Module Impl_core_clone_Clone_for_core_fmt_rt_Flag.
      Definition Self : Ty.t := Ty.path "core::fmt::rt::Flag".
      
      (* 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.read (| self |) |)))
        | _, _, _ => 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_fmt_rt_Flag.
    
    (*
    Enum ArgumentType
    {
      const_params := [];
      ty_params := [];
      variants :=
        [
          {
            name := "Placeholder";
            item :=
              StructRecord
                [
                  ("value", Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ Ty.tuple [] ]);
                  ("formatter",
                    Ty.function
                      [
                        Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ Ty.tuple [] ];
                        Ty.apply (Ty.path "&mut") [] [ Ty.path "core::fmt::Formatter" ]
                      ]
                      (Ty.apply
                        (Ty.path "core::result::Result")
                        []
                        [ Ty.tuple []; Ty.path "core::fmt::Error" ]));
                  ("_lifetime",
                    Ty.apply
                      (Ty.path "core::marker::PhantomData")
                      []
                      [ Ty.apply (Ty.path "&") [] [ Ty.tuple [] ] ])
                ];
            discriminant := None;
          };
          {
            name := "Count";
            item := StructTuple [ Ty.path "usize" ];
            discriminant := None;
          }
        ];
    }
    *)
    
    Module Impl_core_marker_Copy_for_core_fmt_rt_ArgumentType.
      Definition Self : Ty.t := Ty.path "core::fmt::rt::ArgumentType".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::Copy"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Copy_for_core_fmt_rt_ArgumentType.
    
    Module Impl_core_clone_Clone_for_core_fmt_rt_ArgumentType.
      Definition Self : Ty.t := Ty.path "core::fmt::rt::ArgumentType".
      
      (* 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 (|
                Value.DeclaredButUndefined,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (M.match_operator (|
                        Value.DeclaredButUndefined,
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (M.match_operator (|
                                Value.DeclaredButUndefined,
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (M.match_operator (|
                                        Value.DeclaredButUndefined,
                                        [ fun γ => ltac:(M.monadic (M.read (| self |))) ]
                                      |)))
                                ]
                              |)))
                        ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => 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_fmt_rt_ArgumentType.
    
    (* StructRecord
      {
        name := "Argument";
        const_params := [];
        ty_params := [];
        fields := [ ("ty", Ty.path "core::fmt::rt::ArgumentType") ];
      } *)
    
    Module Impl_core_marker_Copy_for_core_fmt_rt_Argument.
      Definition Self : Ty.t := Ty.path "core::fmt::rt::Argument".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::Copy"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Copy_for_core_fmt_rt_Argument.
    
    Module Impl_core_clone_Clone_for_core_fmt_rt_Argument.
      Definition Self : Ty.t := Ty.path "core::fmt::rt::Argument".
      
      (* 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 (|
                Value.DeclaredButUndefined,
                [ fun γ => ltac:(M.monadic (M.read (| self |))) ]
              |)
            |)))
        | _, _, _ => 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_fmt_rt_Argument.
    
    Module Impl_core_fmt_rt_Argument.
      Definition Self : Ty.t := Ty.path "core::fmt::rt::Argument".
      
      (*
          fn new<'b, T>(x: &'b T, f: fn(&T, &mut Formatter<'_>) -> Result) -> Argument<'b> {
              Argument {
                  // INVARIANT: this creates an `ArgumentType<'b>` from a `&'b T` and
                  // a `fn(&T, ...)`, so the invariant is maintained.
                  ty: ArgumentType::Placeholder {
                      value: NonNull::from(x).cast(),
                      // SAFETY: function pointers always have the same layout.
                      formatter: unsafe { mem::transmute(f) },
                      _lifetime: PhantomData,
                  },
              }
          }
      *)
      Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ T ], [ x; f ] =>
          ltac:(M.monadic
            (let x := M.alloc (| x |) in
            let f := M.alloc (| f |) in
            Value.StructRecord
              "core::fmt::rt::Argument"
              [
                ("ty",
                  Value.StructRecord
                    "core::fmt::rt::ArgumentType::Placeholder"
                    [
                      ("value",
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                            "cast",
                            [ Ty.tuple [] ]
                          |),
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::convert::From",
                                Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                                [ Ty.apply (Ty.path "&") [] [ T ] ],
                                "from",
                                []
                              |),
                              [ M.read (| x |) ]
                            |)
                          ]
                        |));
                      ("formatter",
                        M.call_closure (|
                          M.get_function (|
                            "core::intrinsics::transmute",
                            [
                              Ty.function
                                [
                                  Ty.apply (Ty.path "&") [] [ T ];
                                  Ty.apply (Ty.path "&mut") [] [ Ty.path "core::fmt::Formatter" ]
                                ]
                                (Ty.apply
                                  (Ty.path "core::result::Result")
                                  []
                                  [ Ty.tuple []; Ty.path "core::fmt::Error" ]);
                              Ty.function
                                [
                                  Ty.apply
                                    (Ty.path "core::ptr::non_null::NonNull")
                                    []
                                    [ Ty.tuple [] ];
                                  Ty.apply (Ty.path "&mut") [] [ Ty.path "core::fmt::Formatter" ]
                                ]
                                (Ty.apply
                                  (Ty.path "core::result::Result")
                                  []
                                  [ Ty.tuple []; Ty.path "core::fmt::Error" ])
                            ]
                          |),
                          [ M.read (| f |) ]
                        |));
                      ("_lifetime", Value.StructTuple "core::marker::PhantomData" [])
                    ])
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
      
      (*
          pub fn new_display<'b, T: Display>(x: &'b T) -> Argument<'b> {
              Self::new(x, Display::fmt)
          }
      *)
      Definition new_display (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ T ], [ x ] =>
          ltac:(M.monadic
            (let x := M.alloc (| x |) in
            M.call_closure (|
              M.get_associated_function (| Ty.path "core::fmt::rt::Argument", "new", [ T ] |),
              [
                M.read (| x |);
                (* ReifyFnPointer *)
                M.pointer_coercion (M.get_trait_method (| "core::fmt::Display", T, [], "fmt", [] |))
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new_display : M.IsAssociatedFunction Self "new_display" new_display.
      
      (*
          pub fn new_debug<'b, T: Debug>(x: &'b T) -> Argument<'b> {
              Self::new(x, Debug::fmt)
          }
      *)
      Definition new_debug (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ T ], [ x ] =>
          ltac:(M.monadic
            (let x := M.alloc (| x |) in
            M.call_closure (|
              M.get_associated_function (| Ty.path "core::fmt::rt::Argument", "new", [ T ] |),
              [
                M.read (| x |);
                (* ReifyFnPointer *)
                M.pointer_coercion (M.get_trait_method (| "core::fmt::Debug", T, [], "fmt", [] |))
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new_debug : M.IsAssociatedFunction Self "new_debug" new_debug.
      
      (*
          pub fn new_debug_noop<'b, T: Debug>(x: &'b T) -> Argument<'b> {
              Self::new(x, |_, _| Ok(()))
          }
      *)
      Definition new_debug_noop (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ T ], [ x ] =>
          ltac:(M.monadic
            (let x := M.alloc (| x |) in
            M.call_closure (|
              M.get_associated_function (| Ty.path "core::fmt::rt::Argument", "new", [ T ] |),
              [
                M.read (| x |);
                (* ClosureFnPointer(Safe) *)
                M.pointer_coercion
                  (M.closure
                    (fun γ =>
                      ltac:(M.monadic
                        match γ with
                        | [ α0; α1 ] =>
                          ltac:(M.monadic
                            (M.match_operator (|
                              M.alloc (| α0 |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (M.match_operator (|
                                      M.alloc (| α1 |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (Value.StructTuple
                                              "core::result::Result::Ok"
                                              [ Value.Tuple [] ]))
                                      ]
                                    |)))
                              ]
                            |)))
                        | _ => M.impossible "wrong number of arguments"
                        end)))
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new_debug_noop :
        M.IsAssociatedFunction Self "new_debug_noop" new_debug_noop.
      
      (*
          pub fn new_octal<'b, T: Octal>(x: &'b T) -> Argument<'b> {
              Self::new(x, Octal::fmt)
          }
      *)
      Definition new_octal (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ T ], [ x ] =>
          ltac:(M.monadic
            (let x := M.alloc (| x |) in
            M.call_closure (|
              M.get_associated_function (| Ty.path "core::fmt::rt::Argument", "new", [ T ] |),
              [
                M.read (| x |);
                (* ReifyFnPointer *)
                M.pointer_coercion (M.get_trait_method (| "core::fmt::Octal", T, [], "fmt", [] |))
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new_octal : M.IsAssociatedFunction Self "new_octal" new_octal.
      
      (*
          pub fn new_lower_hex<'b, T: LowerHex>(x: &'b T) -> Argument<'b> {
              Self::new(x, LowerHex::fmt)
          }
      *)
      Definition new_lower_hex (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ T ], [ x ] =>
          ltac:(M.monadic
            (let x := M.alloc (| x |) in
            M.call_closure (|
              M.get_associated_function (| Ty.path "core::fmt::rt::Argument", "new", [ T ] |),
              [
                M.read (| x |);
                (* ReifyFnPointer *)
                M.pointer_coercion
                  (M.get_trait_method (| "core::fmt::LowerHex", T, [], "fmt", [] |))
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new_lower_hex :
        M.IsAssociatedFunction Self "new_lower_hex" new_lower_hex.
      
      (*
          pub fn new_upper_hex<'b, T: UpperHex>(x: &'b T) -> Argument<'b> {
              Self::new(x, UpperHex::fmt)
          }
      *)
      Definition new_upper_hex (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ T ], [ x ] =>
          ltac:(M.monadic
            (let x := M.alloc (| x |) in
            M.call_closure (|
              M.get_associated_function (| Ty.path "core::fmt::rt::Argument", "new", [ T ] |),
              [
                M.read (| x |);
                (* ReifyFnPointer *)
                M.pointer_coercion
                  (M.get_trait_method (| "core::fmt::UpperHex", T, [], "fmt", [] |))
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new_upper_hex :
        M.IsAssociatedFunction Self "new_upper_hex" new_upper_hex.
      
      (*
          pub fn new_pointer<'b, T: Pointer>(x: &'b T) -> Argument<'b> {
              Self::new(x, Pointer::fmt)
          }
      *)
      Definition new_pointer (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ T ], [ x ] =>
          ltac:(M.monadic
            (let x := M.alloc (| x |) in
            M.call_closure (|
              M.get_associated_function (| Ty.path "core::fmt::rt::Argument", "new", [ T ] |),
              [
                M.read (| x |);
                (* ReifyFnPointer *)
                M.pointer_coercion (M.get_trait_method (| "core::fmt::Pointer", T, [], "fmt", [] |))
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new_pointer : M.IsAssociatedFunction Self "new_pointer" new_pointer.
      
      (*
          pub fn new_binary<'b, T: Binary>(x: &'b T) -> Argument<'b> {
              Self::new(x, Binary::fmt)
          }
      *)
      Definition new_binary (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ T ], [ x ] =>
          ltac:(M.monadic
            (let x := M.alloc (| x |) in
            M.call_closure (|
              M.get_associated_function (| Ty.path "core::fmt::rt::Argument", "new", [ T ] |),
              [
                M.read (| x |);
                (* ReifyFnPointer *)
                M.pointer_coercion (M.get_trait_method (| "core::fmt::Binary", T, [], "fmt", [] |))
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new_binary : M.IsAssociatedFunction Self "new_binary" new_binary.
      
      (*
          pub fn new_lower_exp<'b, T: LowerExp>(x: &'b T) -> Argument<'b> {
              Self::new(x, LowerExp::fmt)
          }
      *)
      Definition new_lower_exp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ T ], [ x ] =>
          ltac:(M.monadic
            (let x := M.alloc (| x |) in
            M.call_closure (|
              M.get_associated_function (| Ty.path "core::fmt::rt::Argument", "new", [ T ] |),
              [
                M.read (| x |);
                (* ReifyFnPointer *)
                M.pointer_coercion
                  (M.get_trait_method (| "core::fmt::LowerExp", T, [], "fmt", [] |))
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new_lower_exp :
        M.IsAssociatedFunction Self "new_lower_exp" new_lower_exp.
      
      (*
          pub fn new_upper_exp<'b, T: UpperExp>(x: &'b T) -> Argument<'b> {
              Self::new(x, UpperExp::fmt)
          }
      *)
      Definition new_upper_exp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ T ], [ x ] =>
          ltac:(M.monadic
            (let x := M.alloc (| x |) in
            M.call_closure (|
              M.get_associated_function (| Ty.path "core::fmt::rt::Argument", "new", [ T ] |),
              [
                M.read (| x |);
                (* ReifyFnPointer *)
                M.pointer_coercion
                  (M.get_trait_method (| "core::fmt::UpperExp", T, [], "fmt", [] |))
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new_upper_exp :
        M.IsAssociatedFunction Self "new_upper_exp" new_upper_exp.
      
      (*
          pub fn from_usize(x: &usize) -> Argument<'_> {
              Argument { ty: ArgumentType::Count( *x) }
          }
      *)
      Definition from_usize (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ x ] =>
          ltac:(M.monadic
            (let x := M.alloc (| x |) in
            Value.StructRecord
              "core::fmt::rt::Argument"
              [
                ("ty",
                  Value.StructTuple
                    "core::fmt::rt::ArgumentType::Count"
                    [ M.read (| M.read (| x |) |) ])
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_from_usize : M.IsAssociatedFunction Self "from_usize" from_usize.
      
      (*
          pub(super) unsafe fn fmt(&self, f: &mut Formatter<'_>) -> Result {
              match self.ty {
                  // SAFETY:
                  // Because of the invariant that if `formatter` had the type
                  // `fn(&T, _) -> _` then `value` has type `&'b T` where `'b` is
                  // the lifetime of the `ArgumentType`, and because references
                  // and `NonNull` are ABI-compatible, this is completely equivalent
                  // to calling the original function passed to `new` with the
                  // original reference, which is sound.
                  ArgumentType::Placeholder { formatter, value, .. } => unsafe { formatter(value, f) },
                  // SAFETY: the caller promised this.
                  ArgumentType::Count(_) => unsafe { unreachable_unchecked() },
              }
          }
      *)
      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 (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::fmt::rt::Argument",
                  "ty"
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_record_field (|
                          γ,
                          "core::fmt::rt::ArgumentType::Placeholder",
                          "formatter"
                        |) in
                      let γ0_1 :=
                        M.SubPointer.get_struct_record_field (|
                          γ,
                          "core::fmt::rt::ArgumentType::Placeholder",
                          "value"
                        |) in
                      let formatter := M.copy (| γ0_0 |) in
                      let value := M.copy (| γ0_1 |) in
                      M.alloc (|
                        M.call_closure (|
                          M.read (| formatter |),
                          [ M.read (| value |); M.read (| f |) ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::fmt::rt::ArgumentType::Count",
                          0
                        |) in
                      M.alloc (|
                        M.never_to_any (|
                          M.call_closure (|
                            M.get_function (| "core::hint::unreachable_unchecked", [] |),
                            []
                          |)
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_fmt : M.IsAssociatedFunction Self "fmt" fmt.
      
      (*
          pub(super) fn as_usize(&self) -> Option<usize> {
              match self.ty {
                  ArgumentType::Count(count) => Some(count),
                  ArgumentType::Placeholder { .. } => None,
              }
          }
      *)
      Definition as_usize (ε : 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.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::fmt::rt::Argument",
                  "ty"
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::fmt::rt::ArgumentType::Count",
                          0
                        |) in
                      let count := M.copy (| γ0_0 |) in
                      M.alloc (|
                        Value.StructTuple "core::option::Option::Some" [ M.read (| count |) ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let _ :=
                        M.is_struct_tuple (| γ, "core::fmt::rt::ArgumentType::Placeholder" |) in
                      M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_as_usize : M.IsAssociatedFunction Self "as_usize" as_usize.
      
      (*
          pub fn none() -> [Self; 0] {
              []
          }
      *)
      Definition none (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [] => ltac:(M.monadic (Value.Array []))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_none : M.IsAssociatedFunction Self "none" none.
    End Impl_core_fmt_rt_Argument.
    
    (* StructRecord
      {
        name := "UnsafeArg";
        const_params := [];
        ty_params := [];
        fields := [ ("_private", Ty.tuple []) ];
      } *)
    
    Module Impl_core_fmt_rt_UnsafeArg.
      Definition Self : Ty.t := Ty.path "core::fmt::rt::UnsafeArg".
      
      (*
          pub unsafe fn new() -> Self {
              Self { _private: () }
          }
      *)
      Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [] =>
          ltac:(M.monadic
            (Value.StructRecord "core::fmt::rt::UnsafeArg" [ ("_private", Value.Tuple []) ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
    End Impl_core_fmt_rt_UnsafeArg.
  End rt.
End fmt.
