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

Module time.
  Definition value_NANOS_PER_SEC : Value.t :=
    M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U32 1000000000 |))).
  
  Definition value_NANOS_PER_MILLI : Value.t :=
    M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U32 1000000 |))).
  
  Definition value_NANOS_PER_MICRO : Value.t :=
    M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U32 1000 |))).
  
  Definition value_MILLIS_PER_SEC : Value.t :=
    M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U64 1000 |))).
  
  Definition value_MICROS_PER_SEC : Value.t :=
    M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U64 1000000 |))).
  
  Definition value_SECS_PER_MINUTE : Value.t :=
    M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U64 60 |))).
  
  Definition value_MINS_PER_HOUR : Value.t :=
    M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U64 60 |))).
  
  Definition value_HOURS_PER_DAY : Value.t :=
    M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U64 24 |))).
  
  Definition value_DAYS_PER_WEEK : Value.t :=
    M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U64 7 |))).
  
  (* StructTuple
    {
      name := "Nanoseconds";
      const_params := [];
      ty_params := [];
      fields := [ Ty.path "u32" ];
    } *)
  
  Module Impl_core_clone_Clone_for_core_time_Nanoseconds.
    Definition Self : Ty.t := Ty.path "core::time::Nanoseconds".
    
    (* 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_time_Nanoseconds.
  
  Module Impl_core_marker_Copy_for_core_time_Nanoseconds.
    Definition Self : Ty.t := Ty.path "core::time::Nanoseconds".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::Copy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_for_core_time_Nanoseconds.
  
  Module Impl_core_marker_StructuralPartialEq_for_core_time_Nanoseconds.
    Definition Self : Ty.t := Ty.path "core::time::Nanoseconds".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_core_time_Nanoseconds.
  
  Module Impl_core_cmp_PartialEq_for_core_time_Nanoseconds.
    Definition Self : Ty.t := Ty.path "core::time::Nanoseconds".
    
    (* 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
          BinOp.eq (|
            M.read (|
              M.SubPointer.get_struct_tuple_field (|
                M.read (| self |),
                "core::time::Nanoseconds",
                0
              |)
            |),
            M.read (|
              M.SubPointer.get_struct_tuple_field (|
                M.read (| other |),
                "core::time::Nanoseconds",
                0
              |)
            |)
          |)))
      | _, _, _ => 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_time_Nanoseconds.
  
  Module Impl_core_cmp_Eq_for_core_time_Nanoseconds.
    Definition Self : Ty.t := Ty.path "core::time::Nanoseconds".
    
    (* Eq *)
    Definition assert_receiver_is_total_eq
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              Value.DeclaredButUndefined,
              [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::Eq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *)
        [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
  End Impl_core_cmp_Eq_for_core_time_Nanoseconds.
  
  Module Impl_core_cmp_PartialOrd_for_core_time_Nanoseconds.
    Definition Self : Ty.t := Ty.path "core::time::Nanoseconds".
    
    (* PartialOrd *)
    Definition partial_cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::cmp::PartialOrd",
              Ty.path "u32",
              [ Ty.path "u32" ],
              "partial_cmp",
              []
            |),
            [
              M.SubPointer.get_struct_tuple_field (|
                M.read (| self |),
                "core::time::Nanoseconds",
                0
              |);
              M.SubPointer.get_struct_tuple_field (|
                M.read (| other |),
                "core::time::Nanoseconds",
                0
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::PartialOrd"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("partial_cmp", InstanceField.Method partial_cmp) ].
  End Impl_core_cmp_PartialOrd_for_core_time_Nanoseconds.
  
  Module Impl_core_cmp_Ord_for_core_time_Nanoseconds.
    Definition Self : Ty.t := Ty.path "core::time::Nanoseconds".
    
    (* Ord *)
    Definition cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.call_closure (|
            M.get_trait_method (| "core::cmp::Ord", Ty.path "u32", [], "cmp", [] |),
            [
              M.SubPointer.get_struct_tuple_field (|
                M.read (| self |),
                "core::time::Nanoseconds",
                0
              |);
              M.SubPointer.get_struct_tuple_field (|
                M.read (| other |),
                "core::time::Nanoseconds",
                0
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::Ord"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("cmp", InstanceField.Method cmp) ].
  End Impl_core_cmp_Ord_for_core_time_Nanoseconds.
  
  Module Impl_core_hash_Hash_for_core_time_Nanoseconds.
    Definition Self : Ty.t := Ty.path "core::time::Nanoseconds".
    
    (* Hash *)
    Definition hash (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ __H ], [ self; state ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let state := M.alloc (| state |) in
          M.call_closure (|
            M.get_trait_method (| "core::hash::Hash", Ty.path "u32", [], "hash", [ __H ] |),
            [
              M.SubPointer.get_struct_tuple_field (|
                M.read (| self |),
                "core::time::Nanoseconds",
                0
              |);
              M.read (| state |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::hash::Hash"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("hash", InstanceField.Method hash) ].
  End Impl_core_hash_Hash_for_core_time_Nanoseconds.
  
  Module Impl_core_time_Nanoseconds.
    Definition Self : Ty.t := Ty.path "core::time::Nanoseconds".
    
    (*     const ZERO: Self = unsafe { Nanoseconds(0) }; *)
    (* Ty.path "core::time::Nanoseconds" *)
    Definition value_ZERO : Value.t :=
      M.run
        ltac:(M.monadic
          (M.alloc (|
            Value.StructTuple "core::time::Nanoseconds" [ Value.Integer IntegerKind.U32 0 ]
          |))).
    
    Axiom AssociatedConstant_value_ZERO : M.IsAssociatedConstant Self "value_ZERO" value_ZERO.
  End Impl_core_time_Nanoseconds.
  
  Module Impl_core_default_Default_for_core_time_Nanoseconds.
    Definition Self : Ty.t := Ty.path "core::time::Nanoseconds".
    
    (*
        fn default() -> Self {
            Self::ZERO
        }
    *)
    Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] => ltac:(M.monadic (M.read (| M.get_constant (| "core::time::ZERO" |) |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::default::Default"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method default) ].
  End Impl_core_default_Default_for_core_time_Nanoseconds.
  
  (* StructRecord
    {
      name := "Duration";
      const_params := [];
      ty_params := [];
      fields := [ ("secs", Ty.path "u64"); ("nanos", Ty.path "core::time::Nanoseconds") ];
    } *)
  
  Module Impl_core_clone_Clone_for_core_time_Duration.
    Definition Self : Ty.t := Ty.path "core::time::Duration".
    
    (* 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.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_time_Duration.
  
  Module Impl_core_marker_Copy_for_core_time_Duration.
    Definition Self : Ty.t := Ty.path "core::time::Duration".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::Copy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_for_core_time_Duration.
  
  Module Impl_core_marker_StructuralPartialEq_for_core_time_Duration.
    Definition Self : Ty.t := Ty.path "core::time::Duration".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_core_time_Duration.
  
  Module Impl_core_cmp_PartialEq_for_core_time_Duration.
    Definition Self : Ty.t := Ty.path "core::time::Duration".
    
    (* 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
          LogicalOp.and (|
            BinOp.eq (|
              M.read (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::time::Duration",
                  "secs"
                |)
              |),
              M.read (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| other |),
                  "core::time::Duration",
                  "secs"
                |)
              |)
            |),
            ltac:(M.monadic
              (M.call_closure (|
                M.get_trait_method (|
                  "core::cmp::PartialEq",
                  Ty.path "core::time::Nanoseconds",
                  [ Ty.path "core::time::Nanoseconds" ],
                  "eq",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::time::Duration",
                    "nanos"
                  |);
                  M.SubPointer.get_struct_record_field (|
                    M.read (| other |),
                    "core::time::Duration",
                    "nanos"
                  |)
                ]
              |)))
          |)))
      | _, _, _ => 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_time_Duration.
  
  Module Impl_core_cmp_Eq_for_core_time_Duration.
    Definition Self : Ty.t := Ty.path "core::time::Duration".
    
    (* Eq *)
    Definition assert_receiver_is_total_eq
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              Value.DeclaredButUndefined,
              [
                fun γ =>
                  ltac:(M.monadic
                    (M.match_operator (|
                      Value.DeclaredButUndefined,
                      [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::Eq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *)
        [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
  End Impl_core_cmp_Eq_for_core_time_Duration.
  
  Module Impl_core_cmp_PartialOrd_for_core_time_Duration.
    Definition Self : Ty.t := Ty.path "core::time::Duration".
    
    (* PartialOrd *)
    Definition partial_cmp (ε : 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 (|
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::cmp::PartialOrd",
                    Ty.path "u64",
                    [ Ty.path "u64" ],
                    "partial_cmp",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::time::Duration",
                      "secs"
                    |);
                    M.SubPointer.get_struct_record_field (|
                      M.read (| other |),
                      "core::time::Duration",
                      "secs"
                    |)
                  ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let _ := M.is_struct_tuple (| γ0_0, "core::cmp::Ordering::Equal" |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::cmp::PartialOrd",
                          Ty.path "core::time::Nanoseconds",
                          [ Ty.path "core::time::Nanoseconds" ],
                          "partial_cmp",
                          []
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "core::time::Duration",
                            "nanos"
                          |);
                          M.SubPointer.get_struct_record_field (|
                            M.read (| other |),
                            "core::time::Duration",
                            "nanos"
                          |)
                        ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let cmp := M.copy (| γ |) in
                    cmp))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::PartialOrd"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("partial_cmp", InstanceField.Method partial_cmp) ].
  End Impl_core_cmp_PartialOrd_for_core_time_Duration.
  
  Module Impl_core_cmp_Ord_for_core_time_Duration.
    Definition Self : Ty.t := Ty.path "core::time::Duration".
    
    (* Ord *)
    Definition cmp (ε : 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 (|
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (| "core::cmp::Ord", Ty.path "u64", [], "cmp", [] |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::time::Duration",
                      "secs"
                    |);
                    M.SubPointer.get_struct_record_field (|
                      M.read (| other |),
                      "core::time::Duration",
                      "secs"
                    |)
                  ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::cmp::Ordering::Equal" |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::cmp::Ord",
                          Ty.path "core::time::Nanoseconds",
                          [],
                          "cmp",
                          []
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "core::time::Duration",
                            "nanos"
                          |);
                          M.SubPointer.get_struct_record_field (|
                            M.read (| other |),
                            "core::time::Duration",
                            "nanos"
                          |)
                        ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let cmp := M.copy (| γ |) in
                    cmp))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::Ord"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("cmp", InstanceField.Method cmp) ].
  End Impl_core_cmp_Ord_for_core_time_Duration.
  
  Module Impl_core_hash_Hash_for_core_time_Duration.
    Definition Self : Ty.t := Ty.path "core::time::Duration".
    
    (* Hash *)
    Definition hash (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ __H ], [ self; state ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let state := M.alloc (| state |) in
          M.read (|
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (| "core::hash::Hash", Ty.path "u64", [], "hash", [ __H ] |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::time::Duration",
                      "secs"
                    |);
                    M.read (| state |)
                  ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::hash::Hash",
                  Ty.path "core::time::Nanoseconds",
                  [],
                  "hash",
                  [ __H ]
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::time::Duration",
                    "nanos"
                  |);
                  M.read (| state |)
                ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::hash::Hash"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("hash", InstanceField.Method hash) ].
  End Impl_core_hash_Hash_for_core_time_Duration.
  
  Module Impl_core_default_Default_for_core_time_Duration.
    Definition Self : Ty.t := Ty.path "core::time::Duration".
    
    (* Default *)
    Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.StructRecord
            "core::time::Duration"
            [
              ("secs",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::default::Default",
                    Ty.path "u64",
                    [],
                    "default",
                    []
                  |),
                  []
                |));
              ("nanos",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::default::Default",
                    Ty.path "core::time::Nanoseconds",
                    [],
                    "default",
                    []
                  |),
                  []
                |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::default::Default"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method default) ].
  End Impl_core_default_Default_for_core_time_Duration.
  
  Module Impl_core_time_Duration.
    Definition Self : Ty.t := Ty.path "core::time::Duration".
    
    (*     pub const SECOND: Duration = Duration::from_secs(1); *)
    (* Ty.path "core::time::Duration" *)
    Definition value_SECOND : Value.t :=
      M.run
        ltac:(M.monadic
          (M.alloc (|
            M.call_closure (|
              M.get_associated_function (| Ty.path "core::time::Duration", "from_secs", [] |),
              [ Value.Integer IntegerKind.U64 1 ]
            |)
          |))).
    
    Axiom AssociatedConstant_value_SECOND : M.IsAssociatedConstant Self "value_SECOND" value_SECOND.
    
    (*     pub const MILLISECOND: Duration = Duration::from_millis(1); *)
    (* Ty.path "core::time::Duration" *)
    Definition value_MILLISECOND : Value.t :=
      M.run
        ltac:(M.monadic
          (M.alloc (|
            M.call_closure (|
              M.get_associated_function (| Ty.path "core::time::Duration", "from_millis", [] |),
              [ Value.Integer IntegerKind.U64 1 ]
            |)
          |))).
    
    Axiom AssociatedConstant_value_MILLISECOND :
      M.IsAssociatedConstant Self "value_MILLISECOND" value_MILLISECOND.
    
    (*     pub const MICROSECOND: Duration = Duration::from_micros(1); *)
    (* Ty.path "core::time::Duration" *)
    Definition value_MICROSECOND : Value.t :=
      M.run
        ltac:(M.monadic
          (M.alloc (|
            M.call_closure (|
              M.get_associated_function (| Ty.path "core::time::Duration", "from_micros", [] |),
              [ Value.Integer IntegerKind.U64 1 ]
            |)
          |))).
    
    Axiom AssociatedConstant_value_MICROSECOND :
      M.IsAssociatedConstant Self "value_MICROSECOND" value_MICROSECOND.
    
    (*     pub const NANOSECOND: Duration = Duration::from_nanos(1); *)
    (* Ty.path "core::time::Duration" *)
    Definition value_NANOSECOND : Value.t :=
      M.run
        ltac:(M.monadic
          (M.alloc (|
            M.call_closure (|
              M.get_associated_function (| Ty.path "core::time::Duration", "from_nanos", [] |),
              [ Value.Integer IntegerKind.U64 1 ]
            |)
          |))).
    
    Axiom AssociatedConstant_value_NANOSECOND :
      M.IsAssociatedConstant Self "value_NANOSECOND" value_NANOSECOND.
    
    (*     pub const ZERO: Duration = Duration::from_nanos(0); *)
    (* Ty.path "core::time::Duration" *)
    Definition value_ZERO : Value.t :=
      M.run
        ltac:(M.monadic
          (M.alloc (|
            M.call_closure (|
              M.get_associated_function (| Ty.path "core::time::Duration", "from_nanos", [] |),
              [ Value.Integer IntegerKind.U64 0 ]
            |)
          |))).
    
    Axiom AssociatedConstant_value_ZERO : M.IsAssociatedConstant Self "value_ZERO" value_ZERO.
    
    (*     pub const MAX: Duration = Duration::new(u64::MAX, NANOS_PER_SEC - 1); *)
    (* Ty.path "core::time::Duration" *)
    Definition value_MAX : Value.t :=
      M.run
        ltac:(M.monadic
          (M.alloc (|
            M.call_closure (|
              M.get_associated_function (| Ty.path "core::time::Duration", "new", [] |),
              [
                M.read (| M.get_constant (| "core::num::MAX" |) |);
                BinOp.Wrap.sub (|
                  M.read (| M.get_constant (| "core::time::NANOS_PER_SEC" |) |),
                  Value.Integer IntegerKind.U32 1
                |)
              ]
            |)
          |))).
    
    Axiom AssociatedConstant_value_MAX : M.IsAssociatedConstant Self "value_MAX" value_MAX.
    
    (*
        pub const fn new(secs: u64, nanos: u32) -> Duration {
            if nanos < NANOS_PER_SEC {
                // SAFETY: nanos < NANOS_PER_SEC, therefore nanos is within the valid range
                Duration { secs, nanos: unsafe { Nanoseconds(nanos) } }
            } else {
                // FIXME(const-hack): use `.expect` once that is possible.
                let secs = match secs.checked_add((nanos / NANOS_PER_SEC) as u64) {
                    Some(secs) => secs,
                    None => panic!("overflow in Duration::new"),
                };
                let nanos = nanos % NANOS_PER_SEC;
                // SAFETY: nanos % NANOS_PER_SEC < NANOS_PER_SEC, therefore nanos is within the valid range
                Duration { secs, nanos: unsafe { Nanoseconds(nanos) } }
            }
        }
    *)
    Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ secs; nanos ] =>
        ltac:(M.monadic
          (let secs := M.alloc (| secs |) in
          let nanos := M.alloc (| nanos |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          BinOp.lt (|
                            M.read (| nanos |),
                            M.read (| M.get_constant (| "core::time::NANOS_PER_SEC" |) |)
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      Value.StructRecord
                        "core::time::Duration"
                        [
                          ("secs", M.read (| secs |));
                          ("nanos",
                            Value.StructTuple "core::time::Nanoseconds" [ M.read (| nanos |) ])
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let~ secs :=
                      M.copy (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (| Ty.path "u64", "checked_add", [] |),
                              [
                                M.read (| secs |);
                                M.rust_cast
                                  (BinOp.Wrap.div (|
                                    M.read (| nanos |),
                                    M.read (| M.get_constant (| "core::time::NANOS_PER_SEC" |) |)
                                  |))
                              ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::option::Option::Some",
                                    0
                                  |) in
                                let secs := M.copy (| γ0_0 |) in
                                secs));
                            fun γ =>
                              ltac:(M.monadic
                                (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.call_closure (|
                                      M.get_function (| "core::panicking::panic_fmt", [] |),
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "core::fmt::Arguments",
                                            "new_const",
                                            []
                                          |),
                                          [
                                            M.alloc (|
                                              Value.Array
                                                [
                                                  M.read (|
                                                    Value.String "overflow in Duration::new"
                                                  |)
                                                ]
                                            |)
                                          ]
                                        |)
                                      ]
                                    |)
                                  |)
                                |)))
                          ]
                        |)
                      |) in
                    let~ nanos :=
                      M.alloc (|
                        BinOp.Wrap.rem (|
                          M.read (| nanos |),
                          M.read (| M.get_constant (| "core::time::NANOS_PER_SEC" |) |)
                        |)
                      |) in
                    M.alloc (|
                      Value.StructRecord
                        "core::time::Duration"
                        [
                          ("secs", M.read (| secs |));
                          ("nanos",
                            Value.StructTuple "core::time::Nanoseconds" [ M.read (| nanos |) ])
                        ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
    
    (*
        pub const fn from_secs(secs: u64) -> Duration {
            Duration { secs, nanos: Nanoseconds::ZERO }
        }
    *)
    Definition from_secs (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ secs ] =>
        ltac:(M.monadic
          (let secs := M.alloc (| secs |) in
          Value.StructRecord
            "core::time::Duration"
            [
              ("secs", M.read (| secs |));
              ("nanos", M.read (| M.get_constant (| "core::time::ZERO" |) |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_from_secs : M.IsAssociatedFunction Self "from_secs" from_secs.
    
    (*
        pub const fn from_millis(millis: u64) -> Duration {
            let secs = millis / MILLIS_PER_SEC;
            let subsec_millis = (millis % MILLIS_PER_SEC) as u32;
            // SAFETY: (x % 1_000) * 1_000_000 < 1_000_000_000
            //         => x % 1_000 < 1_000
            let subsec_nanos = unsafe { Nanoseconds(subsec_millis * NANOS_PER_MILLI) };
    
            Duration { secs, nanos: subsec_nanos }
        }
    *)
    Definition from_millis (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ millis ] =>
        ltac:(M.monadic
          (let millis := M.alloc (| millis |) in
          M.read (|
            let~ secs :=
              M.alloc (|
                BinOp.Wrap.div (|
                  M.read (| millis |),
                  M.read (| M.get_constant (| "core::time::MILLIS_PER_SEC" |) |)
                |)
              |) in
            let~ subsec_millis :=
              M.alloc (|
                M.rust_cast
                  (BinOp.Wrap.rem (|
                    M.read (| millis |),
                    M.read (| M.get_constant (| "core::time::MILLIS_PER_SEC" |) |)
                  |))
              |) in
            let~ subsec_nanos :=
              M.alloc (|
                Value.StructTuple
                  "core::time::Nanoseconds"
                  [
                    BinOp.Wrap.mul (|
                      M.read (| subsec_millis |),
                      M.read (| M.get_constant (| "core::time::NANOS_PER_MILLI" |) |)
                    |)
                  ]
              |) in
            M.alloc (|
              Value.StructRecord
                "core::time::Duration"
                [ ("secs", M.read (| secs |)); ("nanos", M.read (| subsec_nanos |)) ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_from_millis : M.IsAssociatedFunction Self "from_millis" from_millis.
    
    (*
        pub const fn from_micros(micros: u64) -> Duration {
            let secs = micros / MICROS_PER_SEC;
            let subsec_micros = (micros % MICROS_PER_SEC) as u32;
            // SAFETY: (x % 1_000_000) * 1_000 < 1_000_000_000
            //         => x % 1_000_000 < 1_000_000
            let subsec_nanos = unsafe { Nanoseconds(subsec_micros * NANOS_PER_MICRO) };
    
            Duration { secs, nanos: subsec_nanos }
        }
    *)
    Definition from_micros (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ micros ] =>
        ltac:(M.monadic
          (let micros := M.alloc (| micros |) in
          M.read (|
            let~ secs :=
              M.alloc (|
                BinOp.Wrap.div (|
                  M.read (| micros |),
                  M.read (| M.get_constant (| "core::time::MICROS_PER_SEC" |) |)
                |)
              |) in
            let~ subsec_micros :=
              M.alloc (|
                M.rust_cast
                  (BinOp.Wrap.rem (|
                    M.read (| micros |),
                    M.read (| M.get_constant (| "core::time::MICROS_PER_SEC" |) |)
                  |))
              |) in
            let~ subsec_nanos :=
              M.alloc (|
                Value.StructTuple
                  "core::time::Nanoseconds"
                  [
                    BinOp.Wrap.mul (|
                      M.read (| subsec_micros |),
                      M.read (| M.get_constant (| "core::time::NANOS_PER_MICRO" |) |)
                    |)
                  ]
              |) in
            M.alloc (|
              Value.StructRecord
                "core::time::Duration"
                [ ("secs", M.read (| secs |)); ("nanos", M.read (| subsec_nanos |)) ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_from_micros : M.IsAssociatedFunction Self "from_micros" from_micros.
    
    (*
        pub const fn from_nanos(nanos: u64) -> Duration {
            const NANOS_PER_SEC: u64 = self::NANOS_PER_SEC as u64;
            let secs = nanos / NANOS_PER_SEC;
            let subsec_nanos = (nanos % NANOS_PER_SEC) as u32;
            // SAFETY: x % 1_000_000_000 < 1_000_000_000
            let subsec_nanos = unsafe { Nanoseconds(subsec_nanos) };
    
            Duration { secs, nanos: subsec_nanos }
        }
    *)
    Definition from_nanos (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ nanos ] =>
        ltac:(M.monadic
          (let nanos := M.alloc (| nanos |) in
          M.read (|
            let~ secs :=
              M.alloc (|
                BinOp.Wrap.div (|
                  M.read (| nanos |),
                  M.read (| M.get_constant (| "core::time::from_nanos::NANOS_PER_SEC" |) |)
                |)
              |) in
            let~ subsec_nanos :=
              M.alloc (|
                M.rust_cast
                  (BinOp.Wrap.rem (|
                    M.read (| nanos |),
                    M.read (| M.get_constant (| "core::time::from_nanos::NANOS_PER_SEC" |) |)
                  |))
              |) in
            let~ subsec_nanos :=
              M.alloc (|
                Value.StructTuple "core::time::Nanoseconds" [ M.read (| subsec_nanos |) ]
              |) in
            M.alloc (|
              Value.StructRecord
                "core::time::Duration"
                [ ("secs", M.read (| secs |)); ("nanos", M.read (| subsec_nanos |)) ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_from_nanos : M.IsAssociatedFunction Self "from_nanos" from_nanos.
    
    (*
        pub const fn from_weeks(weeks: u64) -> Duration {
            if weeks > u64::MAX / (SECS_PER_MINUTE * MINS_PER_HOUR * HOURS_PER_DAY * DAYS_PER_WEEK) {
                panic!("overflow in Duration::from_weeks");
            }
    
            Duration::from_secs(weeks * MINS_PER_HOUR * SECS_PER_MINUTE * HOURS_PER_DAY * DAYS_PER_WEEK)
        }
    *)
    Definition from_weeks (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ weeks ] =>
        ltac:(M.monadic
          (let weeks := M.alloc (| weeks |) in
          M.read (|
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            BinOp.gt (|
                              M.read (| weeks |),
                              BinOp.Wrap.div (|
                                M.read (| M.get_constant (| "core::num::MAX" |) |),
                                BinOp.Wrap.mul (|
                                  BinOp.Wrap.mul (|
                                    BinOp.Wrap.mul (|
                                      M.read (|
                                        M.get_constant (| "core::time::SECS_PER_MINUTE" |)
                                      |),
                                      M.read (| M.get_constant (| "core::time::MINS_PER_HOUR" |) |)
                                    |),
                                    M.read (| M.get_constant (| "core::time::HOURS_PER_DAY" |) |)
                                  |),
                                  M.read (| M.get_constant (| "core::time::DAYS_PER_WEEK" |) |)
                                |)
                              |)
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        M.never_to_any (|
                          M.call_closure (|
                            M.get_function (| "core::panicking::panic_fmt", [] |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::Arguments",
                                  "new_const",
                                  []
                                |),
                                [
                                  M.alloc (|
                                    Value.Array
                                      [ M.read (| Value.String "overflow in Duration::from_weeks" |)
                                      ]
                                  |)
                                ]
                              |)
                            ]
                          |)
                        |)
                      |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "core::time::Duration", "from_secs", [] |),
                [
                  BinOp.Wrap.mul (|
                    BinOp.Wrap.mul (|
                      BinOp.Wrap.mul (|
                        BinOp.Wrap.mul (|
                          M.read (| weeks |),
                          M.read (| M.get_constant (| "core::time::MINS_PER_HOUR" |) |)
                        |),
                        M.read (| M.get_constant (| "core::time::SECS_PER_MINUTE" |) |)
                      |),
                      M.read (| M.get_constant (| "core::time::HOURS_PER_DAY" |) |)
                    |),
                    M.read (| M.get_constant (| "core::time::DAYS_PER_WEEK" |) |)
                  |)
                ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_from_weeks : M.IsAssociatedFunction Self "from_weeks" from_weeks.
    
    (*
        pub const fn from_days(days: u64) -> Duration {
            if days > u64::MAX / (SECS_PER_MINUTE * MINS_PER_HOUR * HOURS_PER_DAY) {
                panic!("overflow in Duration::from_days");
            }
    
            Duration::from_secs(days * MINS_PER_HOUR * SECS_PER_MINUTE * HOURS_PER_DAY)
        }
    *)
    Definition from_days (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ days ] =>
        ltac:(M.monadic
          (let days := M.alloc (| days |) in
          M.read (|
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            BinOp.gt (|
                              M.read (| days |),
                              BinOp.Wrap.div (|
                                M.read (| M.get_constant (| "core::num::MAX" |) |),
                                BinOp.Wrap.mul (|
                                  BinOp.Wrap.mul (|
                                    M.read (| M.get_constant (| "core::time::SECS_PER_MINUTE" |) |),
                                    M.read (| M.get_constant (| "core::time::MINS_PER_HOUR" |) |)
                                  |),
                                  M.read (| M.get_constant (| "core::time::HOURS_PER_DAY" |) |)
                                |)
                              |)
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        M.never_to_any (|
                          M.call_closure (|
                            M.get_function (| "core::panicking::panic_fmt", [] |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::Arguments",
                                  "new_const",
                                  []
                                |),
                                [
                                  M.alloc (|
                                    Value.Array
                                      [ M.read (| Value.String "overflow in Duration::from_days" |)
                                      ]
                                  |)
                                ]
                              |)
                            ]
                          |)
                        |)
                      |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "core::time::Duration", "from_secs", [] |),
                [
                  BinOp.Wrap.mul (|
                    BinOp.Wrap.mul (|
                      BinOp.Wrap.mul (|
                        M.read (| days |),
                        M.read (| M.get_constant (| "core::time::MINS_PER_HOUR" |) |)
                      |),
                      M.read (| M.get_constant (| "core::time::SECS_PER_MINUTE" |) |)
                    |),
                    M.read (| M.get_constant (| "core::time::HOURS_PER_DAY" |) |)
                  |)
                ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_from_days : M.IsAssociatedFunction Self "from_days" from_days.
    
    (*
        pub const fn from_hours(hours: u64) -> Duration {
            if hours > u64::MAX / (SECS_PER_MINUTE * MINS_PER_HOUR) {
                panic!("overflow in Duration::from_hours");
            }
    
            Duration::from_secs(hours * MINS_PER_HOUR * SECS_PER_MINUTE)
        }
    *)
    Definition from_hours (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ hours ] =>
        ltac:(M.monadic
          (let hours := M.alloc (| hours |) in
          M.read (|
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            BinOp.gt (|
                              M.read (| hours |),
                              BinOp.Wrap.div (|
                                M.read (| M.get_constant (| "core::num::MAX" |) |),
                                BinOp.Wrap.mul (|
                                  M.read (| M.get_constant (| "core::time::SECS_PER_MINUTE" |) |),
                                  M.read (| M.get_constant (| "core::time::MINS_PER_HOUR" |) |)
                                |)
                              |)
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        M.never_to_any (|
                          M.call_closure (|
                            M.get_function (| "core::panicking::panic_fmt", [] |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::Arguments",
                                  "new_const",
                                  []
                                |),
                                [
                                  M.alloc (|
                                    Value.Array
                                      [ M.read (| Value.String "overflow in Duration::from_hours" |)
                                      ]
                                  |)
                                ]
                              |)
                            ]
                          |)
                        |)
                      |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "core::time::Duration", "from_secs", [] |),
                [
                  BinOp.Wrap.mul (|
                    BinOp.Wrap.mul (|
                      M.read (| hours |),
                      M.read (| M.get_constant (| "core::time::MINS_PER_HOUR" |) |)
                    |),
                    M.read (| M.get_constant (| "core::time::SECS_PER_MINUTE" |) |)
                  |)
                ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_from_hours : M.IsAssociatedFunction Self "from_hours" from_hours.
    
    (*
        pub const fn from_mins(mins: u64) -> Duration {
            if mins > u64::MAX / SECS_PER_MINUTE {
                panic!("overflow in Duration::from_mins");
            }
    
            Duration::from_secs(mins * SECS_PER_MINUTE)
        }
    *)
    Definition from_mins (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ mins ] =>
        ltac:(M.monadic
          (let mins := M.alloc (| mins |) in
          M.read (|
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            BinOp.gt (|
                              M.read (| mins |),
                              BinOp.Wrap.div (|
                                M.read (| M.get_constant (| "core::num::MAX" |) |),
                                M.read (| M.get_constant (| "core::time::SECS_PER_MINUTE" |) |)
                              |)
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        M.never_to_any (|
                          M.call_closure (|
                            M.get_function (| "core::panicking::panic_fmt", [] |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::Arguments",
                                  "new_const",
                                  []
                                |),
                                [
                                  M.alloc (|
                                    Value.Array
                                      [ M.read (| Value.String "overflow in Duration::from_mins" |)
                                      ]
                                  |)
                                ]
                              |)
                            ]
                          |)
                        |)
                      |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "core::time::Duration", "from_secs", [] |),
                [
                  BinOp.Wrap.mul (|
                    M.read (| mins |),
                    M.read (| M.get_constant (| "core::time::SECS_PER_MINUTE" |) |)
                  |)
                ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_from_mins : M.IsAssociatedFunction Self "from_mins" from_mins.
    
    (*
        pub const fn is_zero(&self) -> bool {
            self.secs == 0 && self.nanos.0 == 0
        }
    *)
    Definition is_zero (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          LogicalOp.and (|
            BinOp.eq (|
              M.read (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::time::Duration",
                  "secs"
                |)
              |),
              Value.Integer IntegerKind.U64 0
            |),
            ltac:(M.monadic
              (BinOp.eq (|
                M.read (|
                  M.SubPointer.get_struct_tuple_field (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::time::Duration",
                      "nanos"
                    |),
                    "core::time::Nanoseconds",
                    0
                  |)
                |),
                Value.Integer IntegerKind.U32 0
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_zero : M.IsAssociatedFunction Self "is_zero" is_zero.
    
    (*
        pub const fn as_secs(&self) -> u64 {
            self.secs
        }
    *)
    Definition as_secs (ε : 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.SubPointer.get_struct_record_field (|
              M.read (| self |),
              "core::time::Duration",
              "secs"
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_as_secs : M.IsAssociatedFunction Self "as_secs" as_secs.
    
    (*
        pub const fn subsec_millis(&self) -> u32 {
            self.nanos.0 / NANOS_PER_MILLI
        }
    *)
    Definition subsec_millis (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          BinOp.Wrap.div (|
            M.read (|
              M.SubPointer.get_struct_tuple_field (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::time::Duration",
                  "nanos"
                |),
                "core::time::Nanoseconds",
                0
              |)
            |),
            M.read (| M.get_constant (| "core::time::NANOS_PER_MILLI" |) |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_subsec_millis :
      M.IsAssociatedFunction Self "subsec_millis" subsec_millis.
    
    (*
        pub const fn subsec_micros(&self) -> u32 {
            self.nanos.0 / NANOS_PER_MICRO
        }
    *)
    Definition subsec_micros (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          BinOp.Wrap.div (|
            M.read (|
              M.SubPointer.get_struct_tuple_field (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::time::Duration",
                  "nanos"
                |),
                "core::time::Nanoseconds",
                0
              |)
            |),
            M.read (| M.get_constant (| "core::time::NANOS_PER_MICRO" |) |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_subsec_micros :
      M.IsAssociatedFunction Self "subsec_micros" subsec_micros.
    
    (*
        pub const fn subsec_nanos(&self) -> u32 {
            self.nanos.0
        }
    *)
    Definition subsec_nanos (ε : 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.SubPointer.get_struct_tuple_field (|
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::time::Duration",
                "nanos"
              |),
              "core::time::Nanoseconds",
              0
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_subsec_nanos : M.IsAssociatedFunction Self "subsec_nanos" subsec_nanos.
    
    (*
        pub const fn as_millis(&self) -> u128 {
            self.secs as u128 * MILLIS_PER_SEC as u128 + (self.nanos.0 / NANOS_PER_MILLI) as u128
        }
    *)
    Definition as_millis (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          BinOp.Wrap.add (|
            BinOp.Wrap.mul (|
              M.rust_cast
                (M.read (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::time::Duration",
                    "secs"
                  |)
                |)),
              M.rust_cast (M.read (| M.get_constant (| "core::time::MILLIS_PER_SEC" |) |))
            |),
            M.rust_cast
              (BinOp.Wrap.div (|
                M.read (|
                  M.SubPointer.get_struct_tuple_field (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::time::Duration",
                      "nanos"
                    |),
                    "core::time::Nanoseconds",
                    0
                  |)
                |),
                M.read (| M.get_constant (| "core::time::NANOS_PER_MILLI" |) |)
              |))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_as_millis : M.IsAssociatedFunction Self "as_millis" as_millis.
    
    (*
        pub const fn as_micros(&self) -> u128 {
            self.secs as u128 * MICROS_PER_SEC as u128 + (self.nanos.0 / NANOS_PER_MICRO) as u128
        }
    *)
    Definition as_micros (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          BinOp.Wrap.add (|
            BinOp.Wrap.mul (|
              M.rust_cast
                (M.read (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::time::Duration",
                    "secs"
                  |)
                |)),
              M.rust_cast (M.read (| M.get_constant (| "core::time::MICROS_PER_SEC" |) |))
            |),
            M.rust_cast
              (BinOp.Wrap.div (|
                M.read (|
                  M.SubPointer.get_struct_tuple_field (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::time::Duration",
                      "nanos"
                    |),
                    "core::time::Nanoseconds",
                    0
                  |)
                |),
                M.read (| M.get_constant (| "core::time::NANOS_PER_MICRO" |) |)
              |))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_as_micros : M.IsAssociatedFunction Self "as_micros" as_micros.
    
    (*
        pub const fn as_nanos(&self) -> u128 {
            self.secs as u128 * NANOS_PER_SEC as u128 + self.nanos.0 as u128
        }
    *)
    Definition as_nanos (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          BinOp.Wrap.add (|
            BinOp.Wrap.mul (|
              M.rust_cast
                (M.read (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::time::Duration",
                    "secs"
                  |)
                |)),
              M.rust_cast (M.read (| M.get_constant (| "core::time::NANOS_PER_SEC" |) |))
            |),
            M.rust_cast
              (M.read (|
                M.SubPointer.get_struct_tuple_field (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::time::Duration",
                    "nanos"
                  |),
                  "core::time::Nanoseconds",
                  0
                |)
              |))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_as_nanos : M.IsAssociatedFunction Self "as_nanos" as_nanos.
    
    (*
        pub const fn abs_diff(self, other: Duration) -> Duration {
            if let Some(res) = self.checked_sub(other) { res } else { other.checked_sub(self).unwrap() }
        }
    *)
    Definition abs_diff (ε : 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 (|
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::time::Duration",
                            "checked_sub",
                            []
                          |),
                          [ M.read (| self |); M.read (| other |) ]
                        |)
                      |) in
                    let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let res := M.copy (| γ0_0 |) in
                    res));
                fun γ =>
                  ltac:(M.monadic
                    (M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "core::option::Option")
                            []
                            [ Ty.path "core::time::Duration" ],
                          "unwrap",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::time::Duration",
                              "checked_sub",
                              []
                            |),
                            [ M.read (| other |); M.read (| self |) ]
                          |)
                        ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_abs_diff : M.IsAssociatedFunction Self "abs_diff" abs_diff.
    
    (*
        pub const fn checked_add(self, rhs: Duration) -> Option<Duration> {
            if let Some(mut secs) = self.secs.checked_add(rhs.secs) {
                let mut nanos = self.nanos.0 + rhs.nanos.0;
                if nanos >= NANOS_PER_SEC {
                    nanos -= NANOS_PER_SEC;
                    if let Some(new_secs) = secs.checked_add(1) {
                        secs = new_secs;
                    } else {
                        return None;
                    }
                }
                debug_assert!(nanos < NANOS_PER_SEC);
                Some(Duration::new(secs, nanos))
            } else {
                None
            }
        }
    *)
    Definition checked_add (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (| Ty.path "u64", "checked_add", [] |),
                              [
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    self,
                                    "core::time::Duration",
                                    "secs"
                                  |)
                                |);
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    rhs,
                                    "core::time::Duration",
                                    "secs"
                                  |)
                                |)
                              ]
                            |)
                          |) in
                        let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::option::Option::Some",
                            0
                          |) in
                        let secs := M.copy (| γ0_0 |) in
                        let~ nanos :=
                          M.alloc (|
                            BinOp.Wrap.add (|
                              M.read (|
                                M.SubPointer.get_struct_tuple_field (|
                                  M.SubPointer.get_struct_record_field (|
                                    self,
                                    "core::time::Duration",
                                    "nanos"
                                  |),
                                  "core::time::Nanoseconds",
                                  0
                                |)
                              |),
                              M.read (|
                                M.SubPointer.get_struct_tuple_field (|
                                  M.SubPointer.get_struct_record_field (|
                                    rhs,
                                    "core::time::Duration",
                                    "nanos"
                                  |),
                                  "core::time::Nanoseconds",
                                  0
                                |)
                              |)
                            |)
                          |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        BinOp.ge (|
                                          M.read (| nanos |),
                                          M.read (|
                                            M.get_constant (| "core::time::NANOS_PER_SEC" |)
                                          |)
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  let~ _ :=
                                    let β := nanos in
                                    M.write (|
                                      β,
                                      BinOp.Wrap.sub (|
                                        M.read (| β |),
                                        M.read (|
                                          M.get_constant (| "core::time::NANOS_PER_SEC" |)
                                        |)
                                      |)
                                    |) in
                                  M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ :=
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path "u64",
                                                  "checked_add",
                                                  []
                                                |),
                                                [ M.read (| secs |); Value.Integer IntegerKind.U64 1
                                                ]
                                              |)
                                            |) in
                                          let γ0_0 :=
                                            M.SubPointer.get_struct_tuple_field (|
                                              γ,
                                              "core::option::Option::Some",
                                              0
                                            |) in
                                          let new_secs := M.copy (| γ0_0 |) in
                                          let~ _ := M.write (| secs, M.read (| new_secs |) |) in
                                          M.alloc (| Value.Tuple [] |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (M.alloc (|
                                            M.never_to_any (|
                                              M.read (|
                                                M.return_ (|
                                                  Value.StructTuple "core::option::Option::None" []
                                                |)
                                              |)
                                            |)
                                          |)))
                                    ]
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ := M.use (M.alloc (| Value.Bool true |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  let~ _ :=
                                    M.match_operator (|
                                      M.alloc (| Value.Tuple [] |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ :=
                                              M.use
                                                (M.alloc (|
                                                  UnOp.not (|
                                                    BinOp.lt (|
                                                      M.read (| nanos |),
                                                      M.read (|
                                                        M.get_constant (|
                                                          "core::time::NANOS_PER_SEC"
                                                        |)
                                                      |)
                                                    |)
                                                  |)
                                                |)) in
                                            let _ :=
                                              M.is_constant_or_break_match (|
                                                M.read (| γ |),
                                                Value.Bool true
                                              |) in
                                            M.alloc (|
                                              M.never_to_any (|
                                                M.call_closure (|
                                                  M.get_function (| "core::panicking::panic", [] |),
                                                  [
                                                    M.read (|
                                                      Value.String
                                                        "assertion failed: nanos < NANOS_PER_SEC"
                                                    |)
                                                  ]
                                                |)
                                              |)
                                            |)));
                                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                      ]
                                    |) in
                                  M.alloc (| Value.Tuple [] |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |) in
                        M.alloc (|
                          Value.StructTuple
                            "core::option::Option::Some"
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::time::Duration",
                                  "new",
                                  []
                                |),
                                [ M.read (| secs |); M.read (| nanos |) ]
                              |)
                            ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                  ]
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_checked_add : M.IsAssociatedFunction Self "checked_add" checked_add.
    
    (*
        pub const fn saturating_add(self, rhs: Duration) -> Duration {
            match self.checked_add(rhs) {
                Some(res) => res,
                None => Duration::MAX,
            }
        }
    *)
    Definition saturating_add (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.read (|
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "core::time::Duration", "checked_add", [] |),
                  [ M.read (| self |); M.read (| rhs |) ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let res := M.copy (| γ0_0 |) in
                    res));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.get_constant (| "core::time::MAX" |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_saturating_add :
      M.IsAssociatedFunction Self "saturating_add" saturating_add.
    
    (*
        pub const fn checked_sub(self, rhs: Duration) -> Option<Duration> {
            if let Some(mut secs) = self.secs.checked_sub(rhs.secs) {
                let nanos = if self.nanos.0 >= rhs.nanos.0 {
                    self.nanos.0 - rhs.nanos.0
                } else if let Some(sub_secs) = secs.checked_sub(1) {
                    secs = sub_secs;
                    self.nanos.0 + NANOS_PER_SEC - rhs.nanos.0
                } else {
                    return None;
                };
                debug_assert!(nanos < NANOS_PER_SEC);
                Some(Duration::new(secs, nanos))
            } else {
                None
            }
        }
    *)
    Definition checked_sub (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (| Ty.path "u64", "checked_sub", [] |),
                              [
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    self,
                                    "core::time::Duration",
                                    "secs"
                                  |)
                                |);
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    rhs,
                                    "core::time::Duration",
                                    "secs"
                                  |)
                                |)
                              ]
                            |)
                          |) in
                        let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::option::Option::Some",
                            0
                          |) in
                        let secs := M.copy (| γ0_0 |) in
                        let~ nanos :=
                          M.copy (|
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          BinOp.ge (|
                                            M.read (|
                                              M.SubPointer.get_struct_tuple_field (|
                                                M.SubPointer.get_struct_record_field (|
                                                  self,
                                                  "core::time::Duration",
                                                  "nanos"
                                                |),
                                                "core::time::Nanoseconds",
                                                0
                                              |)
                                            |),
                                            M.read (|
                                              M.SubPointer.get_struct_tuple_field (|
                                                M.SubPointer.get_struct_record_field (|
                                                  rhs,
                                                  "core::time::Duration",
                                                  "nanos"
                                                |),
                                                "core::time::Nanoseconds",
                                                0
                                              |)
                                            |)
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    M.alloc (|
                                      BinOp.Wrap.sub (|
                                        M.read (|
                                          M.SubPointer.get_struct_tuple_field (|
                                            M.SubPointer.get_struct_record_field (|
                                              self,
                                              "core::time::Duration",
                                              "nanos"
                                            |),
                                            "core::time::Nanoseconds",
                                            0
                                          |)
                                        |),
                                        M.read (|
                                          M.SubPointer.get_struct_tuple_field (|
                                            M.SubPointer.get_struct_record_field (|
                                              rhs,
                                              "core::time::Duration",
                                              "nanos"
                                            |),
                                            "core::time::Nanoseconds",
                                            0
                                          |)
                                        |)
                                      |)
                                    |)));
                                fun γ =>
                                  ltac:(M.monadic
                                    (M.match_operator (|
                                      M.alloc (| Value.Tuple [] |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ :=
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.path "u64",
                                                    "checked_sub",
                                                    []
                                                  |),
                                                  [
                                                    M.read (| secs |);
                                                    Value.Integer IntegerKind.U64 1
                                                  ]
                                                |)
                                              |) in
                                            let γ0_0 :=
                                              M.SubPointer.get_struct_tuple_field (|
                                                γ,
                                                "core::option::Option::Some",
                                                0
                                              |) in
                                            let sub_secs := M.copy (| γ0_0 |) in
                                            let~ _ := M.write (| secs, M.read (| sub_secs |) |) in
                                            M.alloc (|
                                              BinOp.Wrap.sub (|
                                                BinOp.Wrap.add (|
                                                  M.read (|
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      M.SubPointer.get_struct_record_field (|
                                                        self,
                                                        "core::time::Duration",
                                                        "nanos"
                                                      |),
                                                      "core::time::Nanoseconds",
                                                      0
                                                    |)
                                                  |),
                                                  M.read (|
                                                    M.get_constant (| "core::time::NANOS_PER_SEC" |)
                                                  |)
                                                |),
                                                M.read (|
                                                  M.SubPointer.get_struct_tuple_field (|
                                                    M.SubPointer.get_struct_record_field (|
                                                      rhs,
                                                      "core::time::Duration",
                                                      "nanos"
                                                    |),
                                                    "core::time::Nanoseconds",
                                                    0
                                                  |)
                                                |)
                                              |)
                                            |)));
                                        fun γ =>
                                          ltac:(M.monadic
                                            (M.alloc (|
                                              M.never_to_any (|
                                                M.read (|
                                                  M.return_ (|
                                                    Value.StructTuple
                                                      "core::option::Option::None"
                                                      []
                                                  |)
                                                |)
                                              |)
                                            |)))
                                      ]
                                    |)))
                              ]
                            |)
                          |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ := M.use (M.alloc (| Value.Bool true |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  let~ _ :=
                                    M.match_operator (|
                                      M.alloc (| Value.Tuple [] |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ :=
                                              M.use
                                                (M.alloc (|
                                                  UnOp.not (|
                                                    BinOp.lt (|
                                                      M.read (| nanos |),
                                                      M.read (|
                                                        M.get_constant (|
                                                          "core::time::NANOS_PER_SEC"
                                                        |)
                                                      |)
                                                    |)
                                                  |)
                                                |)) in
                                            let _ :=
                                              M.is_constant_or_break_match (|
                                                M.read (| γ |),
                                                Value.Bool true
                                              |) in
                                            M.alloc (|
                                              M.never_to_any (|
                                                M.call_closure (|
                                                  M.get_function (| "core::panicking::panic", [] |),
                                                  [
                                                    M.read (|
                                                      Value.String
                                                        "assertion failed: nanos < NANOS_PER_SEC"
                                                    |)
                                                  ]
                                                |)
                                              |)
                                            |)));
                                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                      ]
                                    |) in
                                  M.alloc (| Value.Tuple [] |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |) in
                        M.alloc (|
                          Value.StructTuple
                            "core::option::Option::Some"
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::time::Duration",
                                  "new",
                                  []
                                |),
                                [ M.read (| secs |); M.read (| nanos |) ]
                              |)
                            ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                  ]
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_checked_sub : M.IsAssociatedFunction Self "checked_sub" checked_sub.
    
    (*
        pub const fn saturating_sub(self, rhs: Duration) -> Duration {
            match self.checked_sub(rhs) {
                Some(res) => res,
                None => Duration::ZERO,
            }
        }
    *)
    Definition saturating_sub (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.read (|
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "core::time::Duration", "checked_sub", [] |),
                  [ M.read (| self |); M.read (| rhs |) ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let res := M.copy (| γ0_0 |) in
                    res));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.get_constant (| "core::time::ZERO" |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_saturating_sub :
      M.IsAssociatedFunction Self "saturating_sub" saturating_sub.
    
    (*
        pub const fn checked_mul(self, rhs: u32) -> Option<Duration> {
            // Multiply nanoseconds as u64, because it cannot overflow that way.
            let total_nanos = self.nanos.0 as u64 * rhs as u64;
            let extra_secs = total_nanos / (NANOS_PER_SEC as u64);
            let nanos = (total_nanos % (NANOS_PER_SEC as u64)) as u32;
            // FIXME(const-hack): use `and_then` once that is possible.
            if let Some(s) = self.secs.checked_mul(rhs as u64) {
                if let Some(secs) = s.checked_add(extra_secs) {
                    debug_assert!(nanos < NANOS_PER_SEC);
                    return Some(Duration::new(secs, nanos));
                }
            }
            None
        }
    *)
    Definition checked_mul (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ total_nanos :=
                  M.alloc (|
                    BinOp.Wrap.mul (|
                      M.rust_cast
                        (M.read (|
                          M.SubPointer.get_struct_tuple_field (|
                            M.SubPointer.get_struct_record_field (|
                              self,
                              "core::time::Duration",
                              "nanos"
                            |),
                            "core::time::Nanoseconds",
                            0
                          |)
                        |)),
                      M.rust_cast (M.read (| rhs |))
                    |)
                  |) in
                let~ extra_secs :=
                  M.alloc (|
                    BinOp.Wrap.div (|
                      M.read (| total_nanos |),
                      M.rust_cast (M.read (| M.get_constant (| "core::time::NANOS_PER_SEC" |) |))
                    |)
                  |) in
                let~ nanos :=
                  M.alloc (|
                    M.rust_cast
                      (BinOp.Wrap.rem (|
                        M.read (| total_nanos |),
                        M.rust_cast (M.read (| M.get_constant (| "core::time::NANOS_PER_SEC" |) |))
                      |))
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (| Ty.path "u64", "checked_mul", [] |),
                                [
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      self,
                                      "core::time::Duration",
                                      "secs"
                                    |)
                                  |);
                                  M.rust_cast (M.read (| rhs |))
                                ]
                              |)
                            |) in
                          let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "core::option::Option::Some",
                              0
                            |) in
                          let s := M.copy (| γ0_0 |) in
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "u64",
                                          "checked_add",
                                          []
                                        |),
                                        [ M.read (| s |); M.read (| extra_secs |) ]
                                      |)
                                    |) in
                                  let γ0_0 :=
                                    M.SubPointer.get_struct_tuple_field (|
                                      γ,
                                      "core::option::Option::Some",
                                      0
                                    |) in
                                  let secs := M.copy (| γ0_0 |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        let~ _ :=
                                          M.match_operator (|
                                            M.alloc (| Value.Tuple [] |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ := M.use (M.alloc (| Value.Bool true |)) in
                                                  let _ :=
                                                    M.is_constant_or_break_match (|
                                                      M.read (| γ |),
                                                      Value.Bool true
                                                    |) in
                                                  let~ _ :=
                                                    M.match_operator (|
                                                      M.alloc (| Value.Tuple [] |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ :=
                                                              M.use
                                                                (M.alloc (|
                                                                  UnOp.not (|
                                                                    BinOp.lt (|
                                                                      M.read (| nanos |),
                                                                      M.read (|
                                                                        M.get_constant (|
                                                                          "core::time::NANOS_PER_SEC"
                                                                        |)
                                                                      |)
                                                                    |)
                                                                  |)
                                                                |)) in
                                                            let _ :=
                                                              M.is_constant_or_break_match (|
                                                                M.read (| γ |),
                                                                Value.Bool true
                                                              |) in
                                                            M.alloc (|
                                                              M.never_to_any (|
                                                                M.call_closure (|
                                                                  M.get_function (|
                                                                    "core::panicking::panic",
                                                                    []
                                                                  |),
                                                                  [
                                                                    M.read (|
                                                                      Value.String
                                                                        "assertion failed: nanos < NANOS_PER_SEC"
                                                                    |)
                                                                  ]
                                                                |)
                                                              |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (M.alloc (| Value.Tuple [] |)))
                                                      ]
                                                    |) in
                                                  M.alloc (| Value.Tuple [] |)));
                                              fun γ =>
                                                ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                            ]
                                          |) in
                                        M.return_ (|
                                          Value.StructTuple
                                            "core::option::Option::Some"
                                            [
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path "core::time::Duration",
                                                  "new",
                                                  []
                                                |),
                                                [ M.read (| secs |); M.read (| nanos |) ]
                                              |)
                                            ]
                                        |)
                                      |)
                                    |)
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.alloc (| Value.StructTuple "core::option::Option::None" [] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_checked_mul : M.IsAssociatedFunction Self "checked_mul" checked_mul.
    
    (*
        pub const fn saturating_mul(self, rhs: u32) -> Duration {
            match self.checked_mul(rhs) {
                Some(res) => res,
                None => Duration::MAX,
            }
        }
    *)
    Definition saturating_mul (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.read (|
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "core::time::Duration", "checked_mul", [] |),
                  [ M.read (| self |); M.read (| rhs |) ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let res := M.copy (| γ0_0 |) in
                    res));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.get_constant (| "core::time::MAX" |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_saturating_mul :
      M.IsAssociatedFunction Self "saturating_mul" saturating_mul.
    
    (*
        pub const fn checked_div(self, rhs: u32) -> Option<Duration> {
            if rhs != 0 {
                let (secs, extra_secs) = (self.secs / (rhs as u64), self.secs % (rhs as u64));
                let (mut nanos, extra_nanos) = (self.nanos.0 / rhs, self.nanos.0 % rhs);
                nanos +=
                    ((extra_secs * (NANOS_PER_SEC as u64) + extra_nanos as u64) / (rhs as u64)) as u32;
                debug_assert!(nanos < NANOS_PER_SEC);
                Some(Duration::new(secs, nanos))
            } else {
                None
            }
        }
    *)
    Definition checked_div (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          BinOp.ne (| M.read (| rhs |), Value.Integer IntegerKind.U32 0 |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.match_operator (|
                      M.alloc (|
                        Value.Tuple
                          [
                            BinOp.Wrap.div (|
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  self,
                                  "core::time::Duration",
                                  "secs"
                                |)
                              |),
                              M.rust_cast (M.read (| rhs |))
                            |);
                            BinOp.Wrap.rem (|
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  self,
                                  "core::time::Duration",
                                  "secs"
                                |)
                              |),
                              M.rust_cast (M.read (| rhs |))
                            |)
                          ]
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                            let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                            let secs := M.copy (| γ0_0 |) in
                            let extra_secs := M.copy (| γ0_1 |) in
                            M.match_operator (|
                              M.alloc (|
                                Value.Tuple
                                  [
                                    BinOp.Wrap.div (|
                                      M.read (|
                                        M.SubPointer.get_struct_tuple_field (|
                                          M.SubPointer.get_struct_record_field (|
                                            self,
                                            "core::time::Duration",
                                            "nanos"
                                          |),
                                          "core::time::Nanoseconds",
                                          0
                                        |)
                                      |),
                                      M.read (| rhs |)
                                    |);
                                    BinOp.Wrap.rem (|
                                      M.read (|
                                        M.SubPointer.get_struct_tuple_field (|
                                          M.SubPointer.get_struct_record_field (|
                                            self,
                                            "core::time::Duration",
                                            "nanos"
                                          |),
                                          "core::time::Nanoseconds",
                                          0
                                        |)
                                      |),
                                      M.read (| rhs |)
                                    |)
                                  ]
                              |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                                    let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                                    let nanos := M.copy (| γ0_0 |) in
                                    let extra_nanos := M.copy (| γ0_1 |) in
                                    let~ _ :=
                                      let β := nanos in
                                      M.write (|
                                        β,
                                        BinOp.Wrap.add (|
                                          M.read (| β |),
                                          M.rust_cast
                                            (BinOp.Wrap.div (|
                                              BinOp.Wrap.add (|
                                                BinOp.Wrap.mul (|
                                                  M.read (| extra_secs |),
                                                  M.rust_cast
                                                    (M.read (|
                                                      M.get_constant (|
                                                        "core::time::NANOS_PER_SEC"
                                                      |)
                                                    |))
                                                |),
                                                M.rust_cast (M.read (| extra_nanos |))
                                              |),
                                              M.rust_cast (M.read (| rhs |))
                                            |))
                                        |)
                                      |) in
                                    let~ _ :=
                                      M.match_operator (|
                                        M.alloc (| Value.Tuple [] |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ := M.use (M.alloc (| Value.Bool true |)) in
                                              let _ :=
                                                M.is_constant_or_break_match (|
                                                  M.read (| γ |),
                                                  Value.Bool true
                                                |) in
                                              let~ _ :=
                                                M.match_operator (|
                                                  M.alloc (| Value.Tuple [] |),
                                                  [
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (let γ :=
                                                          M.use
                                                            (M.alloc (|
                                                              UnOp.not (|
                                                                BinOp.lt (|
                                                                  M.read (| nanos |),
                                                                  M.read (|
                                                                    M.get_constant (|
                                                                      "core::time::NANOS_PER_SEC"
                                                                    |)
                                                                  |)
                                                                |)
                                                              |)
                                                            |)) in
                                                        let _ :=
                                                          M.is_constant_or_break_match (|
                                                            M.read (| γ |),
                                                            Value.Bool true
                                                          |) in
                                                        M.alloc (|
                                                          M.never_to_any (|
                                                            M.call_closure (|
                                                              M.get_function (|
                                                                "core::panicking::panic",
                                                                []
                                                              |),
                                                              [
                                                                M.read (|
                                                                  Value.String
                                                                    "assertion failed: nanos < NANOS_PER_SEC"
                                                                |)
                                                              ]
                                                            |)
                                                          |)
                                                        |)));
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (M.alloc (| Value.Tuple [] |)))
                                                  ]
                                                |) in
                                              M.alloc (| Value.Tuple [] |)));
                                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                        ]
                                      |) in
                                    M.alloc (|
                                      Value.StructTuple
                                        "core::option::Option::Some"
                                        [
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "core::time::Duration",
                                              "new",
                                              []
                                            |),
                                            [ M.read (| secs |); M.read (| nanos |) ]
                                          |)
                                        ]
                                    |)))
                              ]
                            |)))
                      ]
                    |)));
                fun γ =>
                  ltac:(M.monadic (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_checked_div : M.IsAssociatedFunction Self "checked_div" checked_div.
    
    (*
        pub const fn as_secs_f64(&self) -> f64 {
            (self.secs as f64) + (self.nanos.0 as f64) / (NANOS_PER_SEC as f64)
        }
    *)
    Definition as_secs_f64 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          BinOp.Wrap.add (|
            M.rust_cast
              (M.read (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::time::Duration",
                  "secs"
                |)
              |)),
            BinOp.Wrap.div (|
              M.rust_cast
                (M.read (|
                  M.SubPointer.get_struct_tuple_field (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::time::Duration",
                      "nanos"
                    |),
                    "core::time::Nanoseconds",
                    0
                  |)
                |)),
              M.rust_cast (M.read (| M.get_constant (| "core::time::NANOS_PER_SEC" |) |))
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_as_secs_f64 : M.IsAssociatedFunction Self "as_secs_f64" as_secs_f64.
    
    (*
        pub const fn as_secs_f32(&self) -> f32 {
            (self.secs as f32) + (self.nanos.0 as f32) / (NANOS_PER_SEC as f32)
        }
    *)
    Definition as_secs_f32 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          BinOp.Wrap.add (|
            M.rust_cast
              (M.read (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::time::Duration",
                  "secs"
                |)
              |)),
            BinOp.Wrap.div (|
              M.rust_cast
                (M.read (|
                  M.SubPointer.get_struct_tuple_field (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::time::Duration",
                      "nanos"
                    |),
                    "core::time::Nanoseconds",
                    0
                  |)
                |)),
              M.rust_cast (M.read (| M.get_constant (| "core::time::NANOS_PER_SEC" |) |))
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_as_secs_f32 : M.IsAssociatedFunction Self "as_secs_f32" as_secs_f32.
    
    (*
        pub const fn as_millis_f64(&self) -> f64 {
            (self.secs as f64) * (MILLIS_PER_SEC as f64)
                + (self.nanos.0 as f64) / (NANOS_PER_MILLI as f64)
        }
    *)
    Definition as_millis_f64 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          BinOp.Wrap.add (|
            BinOp.Wrap.mul (|
              M.rust_cast
                (M.read (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::time::Duration",
                    "secs"
                  |)
                |)),
              M.rust_cast (M.read (| M.get_constant (| "core::time::MILLIS_PER_SEC" |) |))
            |),
            BinOp.Wrap.div (|
              M.rust_cast
                (M.read (|
                  M.SubPointer.get_struct_tuple_field (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::time::Duration",
                      "nanos"
                    |),
                    "core::time::Nanoseconds",
                    0
                  |)
                |)),
              M.rust_cast (M.read (| M.get_constant (| "core::time::NANOS_PER_MILLI" |) |))
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_as_millis_f64 :
      M.IsAssociatedFunction Self "as_millis_f64" as_millis_f64.
    
    (*
        pub const fn as_millis_f32(&self) -> f32 {
            (self.secs as f32) * (MILLIS_PER_SEC as f32)
                + (self.nanos.0 as f32) / (NANOS_PER_MILLI as f32)
        }
    *)
    Definition as_millis_f32 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          BinOp.Wrap.add (|
            BinOp.Wrap.mul (|
              M.rust_cast
                (M.read (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::time::Duration",
                    "secs"
                  |)
                |)),
              M.rust_cast (M.read (| M.get_constant (| "core::time::MILLIS_PER_SEC" |) |))
            |),
            BinOp.Wrap.div (|
              M.rust_cast
                (M.read (|
                  M.SubPointer.get_struct_tuple_field (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::time::Duration",
                      "nanos"
                    |),
                    "core::time::Nanoseconds",
                    0
                  |)
                |)),
              M.rust_cast (M.read (| M.get_constant (| "core::time::NANOS_PER_MILLI" |) |))
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_as_millis_f32 :
      M.IsAssociatedFunction Self "as_millis_f32" as_millis_f32.
    
    (*
        pub fn from_secs_f64(secs: f64) -> Duration {
            match Duration::try_from_secs_f64(secs) {
                Ok(v) => v,
                Err(e) => panic!("{}", e.description()),
            }
        }
    *)
    Definition from_secs_f64 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ secs ] =>
        ltac:(M.monadic
          (let secs := M.alloc (| secs |) in
          M.read (|
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "core::time::Duration",
                    "try_from_secs_f64",
                    []
                  |),
                  [ M.read (| secs |) ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Ok", 0 |) in
                    let v := M.copy (| γ0_0 |) in
                    v));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                    let e := M.copy (| γ0_0 |) in
                    M.alloc (|
                      M.never_to_any (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Self,
                            "panic_cold_display.from_secs_f64",
                            []
                          |),
                          [
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::time::TryFromFloatSecsError",
                                  "description",
                                  []
                                |),
                                [ e ]
                              |)
                            |)
                          ]
                        |)
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_from_secs_f64 :
      M.IsAssociatedFunction Self "from_secs_f64" from_secs_f64.
    
    (*
        pub fn from_secs_f32(secs: f32) -> Duration {
            match Duration::try_from_secs_f32(secs) {
                Ok(v) => v,
                Err(e) => panic!("{}", e.description()),
            }
        }
    *)
    Definition from_secs_f32 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ secs ] =>
        ltac:(M.monadic
          (let secs := M.alloc (| secs |) in
          M.read (|
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "core::time::Duration",
                    "try_from_secs_f32",
                    []
                  |),
                  [ M.read (| secs |) ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Ok", 0 |) in
                    let v := M.copy (| γ0_0 |) in
                    v));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                    let e := M.copy (| γ0_0 |) in
                    M.alloc (|
                      M.never_to_any (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Self,
                            "panic_cold_display.from_secs_f32",
                            []
                          |),
                          [
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::time::TryFromFloatSecsError",
                                  "description",
                                  []
                                |),
                                [ e ]
                              |)
                            |)
                          ]
                        |)
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_from_secs_f32 :
      M.IsAssociatedFunction Self "from_secs_f32" from_secs_f32.
    
    (*
        pub fn mul_f64(self, rhs: f64) -> Duration {
            Duration::from_secs_f64(rhs * self.as_secs_f64())
        }
    *)
    Definition mul_f64 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.call_closure (|
            M.get_associated_function (| Ty.path "core::time::Duration", "from_secs_f64", [] |),
            [
              BinOp.Wrap.mul (|
                M.read (| rhs |),
                M.call_closure (|
                  M.get_associated_function (| Ty.path "core::time::Duration", "as_secs_f64", [] |),
                  [ self ]
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_mul_f64 : M.IsAssociatedFunction Self "mul_f64" mul_f64.
    
    (*
        pub fn mul_f32(self, rhs: f32) -> Duration {
            Duration::from_secs_f32(rhs * self.as_secs_f32())
        }
    *)
    Definition mul_f32 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.call_closure (|
            M.get_associated_function (| Ty.path "core::time::Duration", "from_secs_f32", [] |),
            [
              BinOp.Wrap.mul (|
                M.read (| rhs |),
                M.call_closure (|
                  M.get_associated_function (| Ty.path "core::time::Duration", "as_secs_f32", [] |),
                  [ self ]
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_mul_f32 : M.IsAssociatedFunction Self "mul_f32" mul_f32.
    
    (*
        pub fn div_f64(self, rhs: f64) -> Duration {
            Duration::from_secs_f64(self.as_secs_f64() / rhs)
        }
    *)
    Definition div_f64 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.call_closure (|
            M.get_associated_function (| Ty.path "core::time::Duration", "from_secs_f64", [] |),
            [
              BinOp.Wrap.div (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "core::time::Duration", "as_secs_f64", [] |),
                  [ self ]
                |),
                M.read (| rhs |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_div_f64 : M.IsAssociatedFunction Self "div_f64" div_f64.
    
    (*
        pub fn div_f32(self, rhs: f32) -> Duration {
            Duration::from_secs_f32(self.as_secs_f32() / rhs)
        }
    *)
    Definition div_f32 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.call_closure (|
            M.get_associated_function (| Ty.path "core::time::Duration", "from_secs_f32", [] |),
            [
              BinOp.Wrap.div (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "core::time::Duration", "as_secs_f32", [] |),
                  [ self ]
                |),
                M.read (| rhs |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_div_f32 : M.IsAssociatedFunction Self "div_f32" div_f32.
    
    (*
        pub const fn div_duration_f64(self, rhs: Duration) -> f64 {
            let self_nanos = (self.secs as f64) * (NANOS_PER_SEC as f64) + (self.nanos.0 as f64);
            let rhs_nanos = (rhs.secs as f64) * (NANOS_PER_SEC as f64) + (rhs.nanos.0 as f64);
            self_nanos / rhs_nanos
        }
    *)
    Definition div_duration_f64 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.read (|
            let~ self_nanos :=
              M.alloc (|
                BinOp.Wrap.add (|
                  BinOp.Wrap.mul (|
                    M.rust_cast
                      (M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::time::Duration",
                          "secs"
                        |)
                      |)),
                    M.rust_cast (M.read (| M.get_constant (| "core::time::NANOS_PER_SEC" |) |))
                  |),
                  M.rust_cast
                    (M.read (|
                      M.SubPointer.get_struct_tuple_field (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::time::Duration",
                          "nanos"
                        |),
                        "core::time::Nanoseconds",
                        0
                      |)
                    |))
                |)
              |) in
            let~ rhs_nanos :=
              M.alloc (|
                BinOp.Wrap.add (|
                  BinOp.Wrap.mul (|
                    M.rust_cast
                      (M.read (|
                        M.SubPointer.get_struct_record_field (|
                          rhs,
                          "core::time::Duration",
                          "secs"
                        |)
                      |)),
                    M.rust_cast (M.read (| M.get_constant (| "core::time::NANOS_PER_SEC" |) |))
                  |),
                  M.rust_cast
                    (M.read (|
                      M.SubPointer.get_struct_tuple_field (|
                        M.SubPointer.get_struct_record_field (|
                          rhs,
                          "core::time::Duration",
                          "nanos"
                        |),
                        "core::time::Nanoseconds",
                        0
                      |)
                    |))
                |)
              |) in
            M.alloc (| BinOp.Wrap.div (| M.read (| self_nanos |), M.read (| rhs_nanos |) |) |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_div_duration_f64 :
      M.IsAssociatedFunction Self "div_duration_f64" div_duration_f64.
    
    (*
        pub const fn div_duration_f32(self, rhs: Duration) -> f32 {
            let self_nanos = (self.secs as f32) * (NANOS_PER_SEC as f32) + (self.nanos.0 as f32);
            let rhs_nanos = (rhs.secs as f32) * (NANOS_PER_SEC as f32) + (rhs.nanos.0 as f32);
            self_nanos / rhs_nanos
        }
    *)
    Definition div_duration_f32 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.read (|
            let~ self_nanos :=
              M.alloc (|
                BinOp.Wrap.add (|
                  BinOp.Wrap.mul (|
                    M.rust_cast
                      (M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::time::Duration",
                          "secs"
                        |)
                      |)),
                    M.rust_cast (M.read (| M.get_constant (| "core::time::NANOS_PER_SEC" |) |))
                  |),
                  M.rust_cast
                    (M.read (|
                      M.SubPointer.get_struct_tuple_field (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::time::Duration",
                          "nanos"
                        |),
                        "core::time::Nanoseconds",
                        0
                      |)
                    |))
                |)
              |) in
            let~ rhs_nanos :=
              M.alloc (|
                BinOp.Wrap.add (|
                  BinOp.Wrap.mul (|
                    M.rust_cast
                      (M.read (|
                        M.SubPointer.get_struct_record_field (|
                          rhs,
                          "core::time::Duration",
                          "secs"
                        |)
                      |)),
                    M.rust_cast (M.read (| M.get_constant (| "core::time::NANOS_PER_SEC" |) |))
                  |),
                  M.rust_cast
                    (M.read (|
                      M.SubPointer.get_struct_tuple_field (|
                        M.SubPointer.get_struct_record_field (|
                          rhs,
                          "core::time::Duration",
                          "nanos"
                        |),
                        "core::time::Nanoseconds",
                        0
                      |)
                    |))
                |)
              |) in
            M.alloc (| BinOp.Wrap.div (| M.read (| self_nanos |), M.read (| rhs_nanos |) |) |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_div_duration_f32 :
      M.IsAssociatedFunction Self "div_duration_f32" div_duration_f32.
    (*
        pub fn try_from_secs_f32(secs: f32) -> Result<Duration, TryFromFloatSecsError> {
            try_from_secs!(
                secs = secs,
                mantissa_bits = 23,
                exponent_bits = 8,
                offset = 41,
                bits_ty = u32,
                double_ty = u64,
            )
        }
    *)
    Definition try_from_secs_f32 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ secs ] =>
        ltac:(M.monadic
          (let secs := M.alloc (| secs |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.lt (| M.read (| secs |), M.read (| UnsupportedLiteral |) |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                M.return_ (|
                                  Value.StructTuple
                                    "core::result::Result::Err"
                                    [
                                      Value.StructRecord
                                        "core::time::TryFromFloatSecsError"
                                        [
                                          ("kind",
                                            Value.StructTuple
                                              "core::time::TryFromFloatSecsErrorKind::Negative"
                                              [])
                                        ]
                                    ]
                                |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ bits :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "f32", "to_bits", [] |),
                      [ M.read (| secs |) ]
                    |)
                  |) in
                let~ mant :=
                  M.alloc (|
                    BinOp.bit_or
                      (BinOp.bit_and
                        (M.read (| bits |))
                        (M.read (|
                          M.get_constant (| "core::time::try_from_secs_f32::MANT_MASK" |)
                        |)))
                      (BinOp.Wrap.add (|
                        M.read (|
                          M.get_constant (| "core::time::try_from_secs_f32::MANT_MASK" |)
                        |),
                        Value.Integer IntegerKind.U32 1
                      |))
                  |) in
                let~ exp :=
                  M.alloc (|
                    BinOp.Wrap.add (|
                      M.rust_cast
                        (BinOp.bit_and
                          (BinOp.Wrap.shr (| M.read (| bits |), Value.Integer IntegerKind.I32 23 |))
                          (M.read (|
                            M.get_constant (| "core::time::try_from_secs_f32::EXP_MASK" |)
                          |))),
                      M.read (| M.get_constant (| "core::time::try_from_secs_f32::MIN_EXP" |) |)
                    |)
                  |) in
                M.match_operator (|
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.lt (| M.read (| exp |), Value.Integer IntegerKind.I16 (-31) |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            Value.Tuple
                              [ Value.Integer IntegerKind.U64 0; Value.Integer IntegerKind.U32 0 ]
                          |)));
                      fun γ =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        BinOp.lt (|
                                          M.read (| exp |),
                                          Value.Integer IntegerKind.I16 0
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  let~ t :=
                                    M.alloc (|
                                      BinOp.Wrap.shl (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::convert::From",
                                            Ty.path "u64",
                                            [ Ty.path "u32" ],
                                            "from",
                                            []
                                          |),
                                          [ M.read (| mant |) ]
                                        |),
                                        BinOp.Wrap.add (|
                                          Value.Integer IntegerKind.I16 41,
                                          M.read (| exp |)
                                        |)
                                      |)
                                    |) in
                                  let~ nanos_offset :=
                                    M.alloc (|
                                      BinOp.Wrap.add (|
                                        Value.Integer IntegerKind.I32 23,
                                        Value.Integer IntegerKind.I32 41
                                      |)
                                    |) in
                                  let~ nanos_tmp :=
                                    M.alloc (|
                                      BinOp.Wrap.mul (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::convert::From",
                                            Ty.path "u128",
                                            [ Ty.path "u32" ],
                                            "from",
                                            []
                                          |),
                                          [
                                            M.read (|
                                              M.get_constant (| "core::time::NANOS_PER_SEC" |)
                                            |)
                                          ]
                                        |),
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::convert::From",
                                            Ty.path "u128",
                                            [ Ty.path "u64" ],
                                            "from",
                                            []
                                          |),
                                          [ M.read (| t |) ]
                                        |)
                                      |)
                                    |) in
                                  let~ nanos :=
                                    M.alloc (|
                                      M.rust_cast
                                        (BinOp.Wrap.shr (|
                                          M.read (| nanos_tmp |),
                                          M.read (| nanos_offset |)
                                        |))
                                    |) in
                                  let~ rem_mask :=
                                    M.alloc (|
                                      BinOp.Wrap.sub (|
                                        BinOp.Wrap.shl (|
                                          Value.Integer IntegerKind.U128 1,
                                          M.read (| nanos_offset |)
                                        |),
                                        Value.Integer IntegerKind.U128 1
                                      |)
                                    |) in
                                  let~ rem_msb_mask :=
                                    M.alloc (|
                                      BinOp.Wrap.shl (|
                                        Value.Integer IntegerKind.U128 1,
                                        BinOp.Wrap.sub (|
                                          M.read (| nanos_offset |),
                                          Value.Integer IntegerKind.I32 1
                                        |)
                                      |)
                                    |) in
                                  let~ rem :=
                                    M.alloc (|
                                      BinOp.bit_and (M.read (| nanos_tmp |)) (M.read (| rem_mask |))
                                    |) in
                                  let~ is_tie :=
                                    M.alloc (|
                                      BinOp.eq (| M.read (| rem |), M.read (| rem_msb_mask |) |)
                                    |) in
                                  let~ is_even :=
                                    M.alloc (|
                                      BinOp.eq (|
                                        BinOp.bit_and
                                          (M.read (| nanos |))
                                          (Value.Integer IntegerKind.U32 1),
                                        Value.Integer IntegerKind.U32 0
                                      |)
                                    |) in
                                  let~ rem_msb :=
                                    M.alloc (|
                                      BinOp.eq (|
                                        BinOp.bit_and
                                          (M.read (| nanos_tmp |))
                                          (M.read (| rem_msb_mask |)),
                                        Value.Integer IntegerKind.U128 0
                                      |)
                                    |) in
                                  let~ add_ns :=
                                    M.alloc (|
                                      UnOp.not (|
                                        LogicalOp.or (|
                                          M.read (| rem_msb |),
                                          ltac:(M.monadic
                                            (LogicalOp.and (|
                                              M.read (| is_even |),
                                              ltac:(M.monadic (M.read (| is_tie |)))
                                            |)))
                                        |)
                                      |)
                                    |) in
                                  let~ nanos :=
                                    M.alloc (|
                                      BinOp.Wrap.add (|
                                        M.read (| nanos |),
                                        M.rust_cast (M.read (| add_ns |))
                                      |)
                                    |) in
                                  M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ :=
                                            M.use
                                              (M.alloc (|
                                                LogicalOp.or (|
                                                  BinOp.eq (|
                                                    Value.Integer IntegerKind.I32 23,
                                                    Value.Integer IntegerKind.I32 23
                                                  |),
                                                  ltac:(M.monadic
                                                    (BinOp.ne (|
                                                      M.read (| nanos |),
                                                      M.read (|
                                                        M.get_constant (|
                                                          "core::time::NANOS_PER_SEC"
                                                        |)
                                                      |)
                                                    |)))
                                                |)
                                              |)) in
                                          let _ :=
                                            M.is_constant_or_break_match (|
                                              M.read (| γ |),
                                              Value.Bool true
                                            |) in
                                          M.alloc (|
                                            Value.Tuple
                                              [ Value.Integer IntegerKind.U64 0; M.read (| nanos |)
                                              ]
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (M.alloc (|
                                            Value.Tuple
                                              [
                                                Value.Integer IntegerKind.U64 1;
                                                Value.Integer IntegerKind.U32 0
                                              ]
                                          |)))
                                    ]
                                  |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ :=
                                            M.use
                                              (M.alloc (|
                                                BinOp.lt (|
                                                  M.read (| exp |),
                                                  Value.Integer IntegerKind.I16 23
                                                |)
                                              |)) in
                                          let _ :=
                                            M.is_constant_or_break_match (|
                                              M.read (| γ |),
                                              Value.Bool true
                                            |) in
                                          let~ secs :=
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::convert::From",
                                                  Ty.path "u64",
                                                  [ Ty.path "u32" ],
                                                  "from",
                                                  []
                                                |),
                                                [
                                                  BinOp.Wrap.shr (|
                                                    M.read (| mant |),
                                                    BinOp.Wrap.sub (|
                                                      Value.Integer IntegerKind.I16 23,
                                                      M.read (| exp |)
                                                    |)
                                                  |)
                                                ]
                                              |)
                                            |) in
                                          let~ t :=
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::convert::From",
                                                  Ty.path "u64",
                                                  [ Ty.path "u32" ],
                                                  "from",
                                                  []
                                                |),
                                                [
                                                  BinOp.bit_and
                                                    (BinOp.Wrap.shl (|
                                                      M.read (| mant |),
                                                      M.read (| exp |)
                                                    |))
                                                    (M.read (|
                                                      M.get_constant (|
                                                        "core::time::try_from_secs_f32::MANT_MASK"
                                                      |)
                                                    |))
                                                ]
                                              |)
                                            |) in
                                          let~ nanos_offset :=
                                            M.alloc (| Value.Integer IntegerKind.I32 23 |) in
                                          let~ nanos_tmp :=
                                            M.alloc (|
                                              BinOp.Wrap.mul (|
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::convert::From",
                                                    Ty.path "u64",
                                                    [ Ty.path "u32" ],
                                                    "from",
                                                    []
                                                  |),
                                                  [
                                                    M.read (|
                                                      M.get_constant (|
                                                        "core::time::NANOS_PER_SEC"
                                                      |)
                                                    |)
                                                  ]
                                                |),
                                                M.read (| t |)
                                              |)
                                            |) in
                                          let~ nanos :=
                                            M.alloc (|
                                              M.rust_cast
                                                (BinOp.Wrap.shr (|
                                                  M.read (| nanos_tmp |),
                                                  M.read (| nanos_offset |)
                                                |))
                                            |) in
                                          let~ rem_mask :=
                                            M.alloc (|
                                              BinOp.Wrap.sub (|
                                                BinOp.Wrap.shl (|
                                                  Value.Integer IntegerKind.U64 1,
                                                  M.read (| nanos_offset |)
                                                |),
                                                Value.Integer IntegerKind.U64 1
                                              |)
                                            |) in
                                          let~ rem_msb_mask :=
                                            M.alloc (|
                                              BinOp.Wrap.shl (|
                                                Value.Integer IntegerKind.U64 1,
                                                BinOp.Wrap.sub (|
                                                  M.read (| nanos_offset |),
                                                  Value.Integer IntegerKind.I32 1
                                                |)
                                              |)
                                            |) in
                                          let~ rem :=
                                            M.alloc (|
                                              BinOp.bit_and
                                                (M.read (| nanos_tmp |))
                                                (M.read (| rem_mask |))
                                            |) in
                                          let~ is_tie :=
                                            M.alloc (|
                                              BinOp.eq (|
                                                M.read (| rem |),
                                                M.read (| rem_msb_mask |)
                                              |)
                                            |) in
                                          let~ is_even :=
                                            M.alloc (|
                                              BinOp.eq (|
                                                BinOp.bit_and
                                                  (M.read (| nanos |))
                                                  (Value.Integer IntegerKind.U32 1),
                                                Value.Integer IntegerKind.U32 0
                                              |)
                                            |) in
                                          let~ rem_msb :=
                                            M.alloc (|
                                              BinOp.eq (|
                                                BinOp.bit_and
                                                  (M.read (| nanos_tmp |))
                                                  (M.read (| rem_msb_mask |)),
                                                Value.Integer IntegerKind.U64 0
                                              |)
                                            |) in
                                          let~ add_ns :=
                                            M.alloc (|
                                              UnOp.not (|
                                                LogicalOp.or (|
                                                  M.read (| rem_msb |),
                                                  ltac:(M.monadic
                                                    (LogicalOp.and (|
                                                      M.read (| is_even |),
                                                      ltac:(M.monadic (M.read (| is_tie |)))
                                                    |)))
                                                |)
                                              |)
                                            |) in
                                          let~ nanos :=
                                            M.alloc (|
                                              BinOp.Wrap.add (|
                                                M.read (| nanos |),
                                                M.rust_cast (M.read (| add_ns |))
                                              |)
                                            |) in
                                          M.match_operator (|
                                            M.alloc (| Value.Tuple [] |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ :=
                                                    M.use
                                                      (M.alloc (|
                                                        LogicalOp.or (|
                                                          BinOp.eq (|
                                                            Value.Integer IntegerKind.I32 23,
                                                            Value.Integer IntegerKind.I32 23
                                                          |),
                                                          ltac:(M.monadic
                                                            (BinOp.ne (|
                                                              M.read (| nanos |),
                                                              M.read (|
                                                                M.get_constant (|
                                                                  "core::time::NANOS_PER_SEC"
                                                                |)
                                                              |)
                                                            |)))
                                                        |)
                                                      |)) in
                                                  let _ :=
                                                    M.is_constant_or_break_match (|
                                                      M.read (| γ |),
                                                      Value.Bool true
                                                    |) in
                                                  M.alloc (|
                                                    Value.Tuple
                                                      [ M.read (| secs |); M.read (| nanos |) ]
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (M.alloc (|
                                                    Value.Tuple
                                                      [
                                                        BinOp.Wrap.add (|
                                                          M.read (| secs |),
                                                          Value.Integer IntegerKind.U64 1
                                                        |);
                                                        Value.Integer IntegerKind.U32 0
                                                      ]
                                                  |)))
                                            ]
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (M.match_operator (|
                                            M.alloc (| Value.Tuple [] |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ :=
                                                    M.use
                                                      (M.alloc (|
                                                        BinOp.lt (|
                                                          M.read (| exp |),
                                                          Value.Integer IntegerKind.I16 64
                                                        |)
                                                      |)) in
                                                  let _ :=
                                                    M.is_constant_or_break_match (|
                                                      M.read (| γ |),
                                                      Value.Bool true
                                                    |) in
                                                  let~ secs :=
                                                    M.alloc (|
                                                      BinOp.Wrap.shl (|
                                                        M.call_closure (|
                                                          M.get_trait_method (|
                                                            "core::convert::From",
                                                            Ty.path "u64",
                                                            [ Ty.path "u32" ],
                                                            "from",
                                                            []
                                                          |),
                                                          [ M.read (| mant |) ]
                                                        |),
                                                        BinOp.Wrap.sub (|
                                                          M.read (| exp |),
                                                          Value.Integer IntegerKind.I16 23
                                                        |)
                                                      |)
                                                    |) in
                                                  M.alloc (|
                                                    Value.Tuple
                                                      [
                                                        M.read (| secs |);
                                                        Value.Integer IntegerKind.U32 0
                                                      ]
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (M.alloc (|
                                                    M.never_to_any (|
                                                      M.read (|
                                                        M.return_ (|
                                                          Value.StructTuple
                                                            "core::result::Result::Err"
                                                            [
                                                              Value.StructRecord
                                                                "core::time::TryFromFloatSecsError"
                                                                [
                                                                  ("kind",
                                                                    Value.StructTuple
                                                                      "core::time::TryFromFloatSecsErrorKind::OverflowOrNan"
                                                                      [])
                                                                ]
                                                            ]
                                                        |)
                                                      |)
                                                    |)
                                                  |)))
                                            ]
                                          |)))
                                    ]
                                  |)))
                            ]
                          |)))
                    ]
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                        let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                        let secs := M.copy (| γ0_0 |) in
                        let nanos := M.copy (| γ0_1 |) in
                        M.alloc (|
                          Value.StructTuple
                            "core::result::Result::Ok"
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::time::Duration",
                                  "new",
                                  []
                                |),
                                [ M.read (| secs |); M.read (| nanos |) ]
                              |)
                            ]
                        |)))
                  ]
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_try_from_secs_f32 :
      M.IsAssociatedFunction Self "try_from_secs_f32" try_from_secs_f32.
    
    (*
        pub fn try_from_secs_f64(secs: f64) -> Result<Duration, TryFromFloatSecsError> {
            try_from_secs!(
                secs = secs,
                mantissa_bits = 52,
                exponent_bits = 11,
                offset = 44,
                bits_ty = u64,
                double_ty = u128,
            )
        }
    *)
    Definition try_from_secs_f64 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ secs ] =>
        ltac:(M.monadic
          (let secs := M.alloc (| secs |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.lt (| M.read (| secs |), M.read (| UnsupportedLiteral |) |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                M.return_ (|
                                  Value.StructTuple
                                    "core::result::Result::Err"
                                    [
                                      Value.StructRecord
                                        "core::time::TryFromFloatSecsError"
                                        [
                                          ("kind",
                                            Value.StructTuple
                                              "core::time::TryFromFloatSecsErrorKind::Negative"
                                              [])
                                        ]
                                    ]
                                |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ bits :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "f64", "to_bits", [] |),
                      [ M.read (| secs |) ]
                    |)
                  |) in
                let~ mant :=
                  M.alloc (|
                    BinOp.bit_or
                      (BinOp.bit_and
                        (M.read (| bits |))
                        (M.read (|
                          M.get_constant (| "core::time::try_from_secs_f64::MANT_MASK" |)
                        |)))
                      (BinOp.Wrap.add (|
                        M.read (|
                          M.get_constant (| "core::time::try_from_secs_f64::MANT_MASK" |)
                        |),
                        Value.Integer IntegerKind.U64 1
                      |))
                  |) in
                let~ exp :=
                  M.alloc (|
                    BinOp.Wrap.add (|
                      M.rust_cast
                        (BinOp.bit_and
                          (BinOp.Wrap.shr (| M.read (| bits |), Value.Integer IntegerKind.I32 52 |))
                          (M.read (|
                            M.get_constant (| "core::time::try_from_secs_f64::EXP_MASK" |)
                          |))),
                      M.read (| M.get_constant (| "core::time::try_from_secs_f64::MIN_EXP" |) |)
                    |)
                  |) in
                M.match_operator (|
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.lt (| M.read (| exp |), Value.Integer IntegerKind.I16 (-31) |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            Value.Tuple
                              [ Value.Integer IntegerKind.U64 0; Value.Integer IntegerKind.U32 0 ]
                          |)));
                      fun γ =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        BinOp.lt (|
                                          M.read (| exp |),
                                          Value.Integer IntegerKind.I16 0
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  let~ t :=
                                    M.alloc (|
                                      BinOp.Wrap.shl (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::convert::From",
                                            Ty.path "u128",
                                            [ Ty.path "u64" ],
                                            "from",
                                            []
                                          |),
                                          [ M.read (| mant |) ]
                                        |),
                                        BinOp.Wrap.add (|
                                          Value.Integer IntegerKind.I16 44,
                                          M.read (| exp |)
                                        |)
                                      |)
                                    |) in
                                  let~ nanos_offset :=
                                    M.alloc (|
                                      BinOp.Wrap.add (|
                                        Value.Integer IntegerKind.I32 52,
                                        Value.Integer IntegerKind.I32 44
                                      |)
                                    |) in
                                  let~ nanos_tmp :=
                                    M.alloc (|
                                      BinOp.Wrap.mul (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::convert::From",
                                            Ty.path "u128",
                                            [ Ty.path "u32" ],
                                            "from",
                                            []
                                          |),
                                          [
                                            M.read (|
                                              M.get_constant (| "core::time::NANOS_PER_SEC" |)
                                            |)
                                          ]
                                        |),
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::convert::From",
                                            Ty.path "u128",
                                            [ Ty.path "u128" ],
                                            "from",
                                            []
                                          |),
                                          [ M.read (| t |) ]
                                        |)
                                      |)
                                    |) in
                                  let~ nanos :=
                                    M.alloc (|
                                      M.rust_cast
                                        (BinOp.Wrap.shr (|
                                          M.read (| nanos_tmp |),
                                          M.read (| nanos_offset |)
                                        |))
                                    |) in
                                  let~ rem_mask :=
                                    M.alloc (|
                                      BinOp.Wrap.sub (|
                                        BinOp.Wrap.shl (|
                                          Value.Integer IntegerKind.U128 1,
                                          M.read (| nanos_offset |)
                                        |),
                                        Value.Integer IntegerKind.U128 1
                                      |)
                                    |) in
                                  let~ rem_msb_mask :=
                                    M.alloc (|
                                      BinOp.Wrap.shl (|
                                        Value.Integer IntegerKind.U128 1,
                                        BinOp.Wrap.sub (|
                                          M.read (| nanos_offset |),
                                          Value.Integer IntegerKind.I32 1
                                        |)
                                      |)
                                    |) in
                                  let~ rem :=
                                    M.alloc (|
                                      BinOp.bit_and (M.read (| nanos_tmp |)) (M.read (| rem_mask |))
                                    |) in
                                  let~ is_tie :=
                                    M.alloc (|
                                      BinOp.eq (| M.read (| rem |), M.read (| rem_msb_mask |) |)
                                    |) in
                                  let~ is_even :=
                                    M.alloc (|
                                      BinOp.eq (|
                                        BinOp.bit_and
                                          (M.read (| nanos |))
                                          (Value.Integer IntegerKind.U32 1),
                                        Value.Integer IntegerKind.U32 0
                                      |)
                                    |) in
                                  let~ rem_msb :=
                                    M.alloc (|
                                      BinOp.eq (|
                                        BinOp.bit_and
                                          (M.read (| nanos_tmp |))
                                          (M.read (| rem_msb_mask |)),
                                        Value.Integer IntegerKind.U128 0
                                      |)
                                    |) in
                                  let~ add_ns :=
                                    M.alloc (|
                                      UnOp.not (|
                                        LogicalOp.or (|
                                          M.read (| rem_msb |),
                                          ltac:(M.monadic
                                            (LogicalOp.and (|
                                              M.read (| is_even |),
                                              ltac:(M.monadic (M.read (| is_tie |)))
                                            |)))
                                        |)
                                      |)
                                    |) in
                                  let~ nanos :=
                                    M.alloc (|
                                      BinOp.Wrap.add (|
                                        M.read (| nanos |),
                                        M.rust_cast (M.read (| add_ns |))
                                      |)
                                    |) in
                                  M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ :=
                                            M.use
                                              (M.alloc (|
                                                LogicalOp.or (|
                                                  BinOp.eq (|
                                                    Value.Integer IntegerKind.I32 52,
                                                    Value.Integer IntegerKind.I32 23
                                                  |),
                                                  ltac:(M.monadic
                                                    (BinOp.ne (|
                                                      M.read (| nanos |),
                                                      M.read (|
                                                        M.get_constant (|
                                                          "core::time::NANOS_PER_SEC"
                                                        |)
                                                      |)
                                                    |)))
                                                |)
                                              |)) in
                                          let _ :=
                                            M.is_constant_or_break_match (|
                                              M.read (| γ |),
                                              Value.Bool true
                                            |) in
                                          M.alloc (|
                                            Value.Tuple
                                              [ Value.Integer IntegerKind.U64 0; M.read (| nanos |)
                                              ]
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (M.alloc (|
                                            Value.Tuple
                                              [
                                                Value.Integer IntegerKind.U64 1;
                                                Value.Integer IntegerKind.U32 0
                                              ]
                                          |)))
                                    ]
                                  |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ :=
                                            M.use
                                              (M.alloc (|
                                                BinOp.lt (|
                                                  M.read (| exp |),
                                                  Value.Integer IntegerKind.I16 52
                                                |)
                                              |)) in
                                          let _ :=
                                            M.is_constant_or_break_match (|
                                              M.read (| γ |),
                                              Value.Bool true
                                            |) in
                                          let~ secs :=
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::convert::From",
                                                  Ty.path "u64",
                                                  [ Ty.path "u64" ],
                                                  "from",
                                                  []
                                                |),
                                                [
                                                  BinOp.Wrap.shr (|
                                                    M.read (| mant |),
                                                    BinOp.Wrap.sub (|
                                                      Value.Integer IntegerKind.I16 52,
                                                      M.read (| exp |)
                                                    |)
                                                  |)
                                                ]
                                              |)
                                            |) in
                                          let~ t :=
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::convert::From",
                                                  Ty.path "u128",
                                                  [ Ty.path "u64" ],
                                                  "from",
                                                  []
                                                |),
                                                [
                                                  BinOp.bit_and
                                                    (BinOp.Wrap.shl (|
                                                      M.read (| mant |),
                                                      M.read (| exp |)
                                                    |))
                                                    (M.read (|
                                                      M.get_constant (|
                                                        "core::time::try_from_secs_f64::MANT_MASK"
                                                      |)
                                                    |))
                                                ]
                                              |)
                                            |) in
                                          let~ nanos_offset :=
                                            M.alloc (| Value.Integer IntegerKind.I32 52 |) in
                                          let~ nanos_tmp :=
                                            M.alloc (|
                                              BinOp.Wrap.mul (|
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::convert::From",
                                                    Ty.path "u128",
                                                    [ Ty.path "u32" ],
                                                    "from",
                                                    []
                                                  |),
                                                  [
                                                    M.read (|
                                                      M.get_constant (|
                                                        "core::time::NANOS_PER_SEC"
                                                      |)
                                                    |)
                                                  ]
                                                |),
                                                M.read (| t |)
                                              |)
                                            |) in
                                          let~ nanos :=
                                            M.alloc (|
                                              M.rust_cast
                                                (BinOp.Wrap.shr (|
                                                  M.read (| nanos_tmp |),
                                                  M.read (| nanos_offset |)
                                                |))
                                            |) in
                                          let~ rem_mask :=
                                            M.alloc (|
                                              BinOp.Wrap.sub (|
                                                BinOp.Wrap.shl (|
                                                  Value.Integer IntegerKind.U128 1,
                                                  M.read (| nanos_offset |)
                                                |),
                                                Value.Integer IntegerKind.U128 1
                                              |)
                                            |) in
                                          let~ rem_msb_mask :=
                                            M.alloc (|
                                              BinOp.Wrap.shl (|
                                                Value.Integer IntegerKind.U128 1,
                                                BinOp.Wrap.sub (|
                                                  M.read (| nanos_offset |),
                                                  Value.Integer IntegerKind.I32 1
                                                |)
                                              |)
                                            |) in
                                          let~ rem :=
                                            M.alloc (|
                                              BinOp.bit_and
                                                (M.read (| nanos_tmp |))
                                                (M.read (| rem_mask |))
                                            |) in
                                          let~ is_tie :=
                                            M.alloc (|
                                              BinOp.eq (|
                                                M.read (| rem |),
                                                M.read (| rem_msb_mask |)
                                              |)
                                            |) in
                                          let~ is_even :=
                                            M.alloc (|
                                              BinOp.eq (|
                                                BinOp.bit_and
                                                  (M.read (| nanos |))
                                                  (Value.Integer IntegerKind.U32 1),
                                                Value.Integer IntegerKind.U32 0
                                              |)
                                            |) in
                                          let~ rem_msb :=
                                            M.alloc (|
                                              BinOp.eq (|
                                                BinOp.bit_and
                                                  (M.read (| nanos_tmp |))
                                                  (M.read (| rem_msb_mask |)),
                                                Value.Integer IntegerKind.U128 0
                                              |)
                                            |) in
                                          let~ add_ns :=
                                            M.alloc (|
                                              UnOp.not (|
                                                LogicalOp.or (|
                                                  M.read (| rem_msb |),
                                                  ltac:(M.monadic
                                                    (LogicalOp.and (|
                                                      M.read (| is_even |),
                                                      ltac:(M.monadic (M.read (| is_tie |)))
                                                    |)))
                                                |)
                                              |)
                                            |) in
                                          let~ nanos :=
                                            M.alloc (|
                                              BinOp.Wrap.add (|
                                                M.read (| nanos |),
                                                M.rust_cast (M.read (| add_ns |))
                                              |)
                                            |) in
                                          M.match_operator (|
                                            M.alloc (| Value.Tuple [] |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ :=
                                                    M.use
                                                      (M.alloc (|
                                                        LogicalOp.or (|
                                                          BinOp.eq (|
                                                            Value.Integer IntegerKind.I32 52,
                                                            Value.Integer IntegerKind.I32 23
                                                          |),
                                                          ltac:(M.monadic
                                                            (BinOp.ne (|
                                                              M.read (| nanos |),
                                                              M.read (|
                                                                M.get_constant (|
                                                                  "core::time::NANOS_PER_SEC"
                                                                |)
                                                              |)
                                                            |)))
                                                        |)
                                                      |)) in
                                                  let _ :=
                                                    M.is_constant_or_break_match (|
                                                      M.read (| γ |),
                                                      Value.Bool true
                                                    |) in
                                                  M.alloc (|
                                                    Value.Tuple
                                                      [ M.read (| secs |); M.read (| nanos |) ]
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (M.alloc (|
                                                    Value.Tuple
                                                      [
                                                        BinOp.Wrap.add (|
                                                          M.read (| secs |),
                                                          Value.Integer IntegerKind.U64 1
                                                        |);
                                                        Value.Integer IntegerKind.U32 0
                                                      ]
                                                  |)))
                                            ]
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (M.match_operator (|
                                            M.alloc (| Value.Tuple [] |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ :=
                                                    M.use
                                                      (M.alloc (|
                                                        BinOp.lt (|
                                                          M.read (| exp |),
                                                          Value.Integer IntegerKind.I16 64
                                                        |)
                                                      |)) in
                                                  let _ :=
                                                    M.is_constant_or_break_match (|
                                                      M.read (| γ |),
                                                      Value.Bool true
                                                    |) in
                                                  let~ secs :=
                                                    M.alloc (|
                                                      BinOp.Wrap.shl (|
                                                        M.call_closure (|
                                                          M.get_trait_method (|
                                                            "core::convert::From",
                                                            Ty.path "u64",
                                                            [ Ty.path "u64" ],
                                                            "from",
                                                            []
                                                          |),
                                                          [ M.read (| mant |) ]
                                                        |),
                                                        BinOp.Wrap.sub (|
                                                          M.read (| exp |),
                                                          Value.Integer IntegerKind.I16 52
                                                        |)
                                                      |)
                                                    |) in
                                                  M.alloc (|
                                                    Value.Tuple
                                                      [
                                                        M.read (| secs |);
                                                        Value.Integer IntegerKind.U32 0
                                                      ]
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (M.alloc (|
                                                    M.never_to_any (|
                                                      M.read (|
                                                        M.return_ (|
                                                          Value.StructTuple
                                                            "core::result::Result::Err"
                                                            [
                                                              Value.StructRecord
                                                                "core::time::TryFromFloatSecsError"
                                                                [
                                                                  ("kind",
                                                                    Value.StructTuple
                                                                      "core::time::TryFromFloatSecsErrorKind::OverflowOrNan"
                                                                      [])
                                                                ]
                                                            ]
                                                        |)
                                                      |)
                                                    |)
                                                  |)))
                                            ]
                                          |)))
                                    ]
                                  |)))
                            ]
                          |)))
                    ]
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                        let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                        let secs := M.copy (| γ0_0 |) in
                        let nanos := M.copy (| γ0_1 |) in
                        M.alloc (|
                          Value.StructTuple
                            "core::result::Result::Ok"
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::time::Duration",
                                  "new",
                                  []
                                |),
                                [ M.read (| secs |); M.read (| nanos |) ]
                              |)
                            ]
                        |)))
                  ]
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_try_from_secs_f64 :
      M.IsAssociatedFunction Self "try_from_secs_f64" try_from_secs_f64.
  End Impl_core_time_Duration.
  
  Module Impl_core_ops_arith_Add_for_core_time_Duration.
    Definition Self : Ty.t := Ty.path "core::time::Duration".
    
    (*     type Output = Duration; *)
    Definition _Output : Ty.t := Ty.path "core::time::Duration".
    
    (*
        fn add(self, rhs: Duration) -> Duration {
            self.checked_add(rhs).expect("overflow when adding durations")
        }
    *)
    Definition add (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "core::time::Duration" ],
              "expect",
              []
            |),
            [
              M.call_closure (|
                M.get_associated_function (| Ty.path "core::time::Duration", "checked_add", [] |),
                [ M.read (| self |); M.read (| rhs |) ]
              |);
              M.read (| Value.String "overflow when adding durations" |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::ops::arith::Add"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("Output", InstanceField.Ty _Output); ("add", InstanceField.Method add) ].
  End Impl_core_ops_arith_Add_for_core_time_Duration.
  
  Module Impl_core_ops_arith_AddAssign_for_core_time_Duration.
    Definition Self : Ty.t := Ty.path "core::time::Duration".
    
    (*
        fn add_assign(&mut self, rhs: Duration) {
            *self = *self + rhs;
        }
    *)
    Definition add_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.read (|
            let~ _ :=
              M.write (|
                M.read (| self |),
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::arith::Add",
                    Ty.path "core::time::Duration",
                    [ Ty.path "core::time::Duration" ],
                    "add",
                    []
                  |),
                  [ M.read (| M.read (| self |) |); M.read (| rhs |) ]
                |)
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::ops::arith::AddAssign"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("add_assign", InstanceField.Method add_assign) ].
  End Impl_core_ops_arith_AddAssign_for_core_time_Duration.
  
  Module Impl_core_ops_arith_Sub_for_core_time_Duration.
    Definition Self : Ty.t := Ty.path "core::time::Duration".
    
    (*     type Output = Duration; *)
    Definition _Output : Ty.t := Ty.path "core::time::Duration".
    
    (*
        fn sub(self, rhs: Duration) -> Duration {
            self.checked_sub(rhs).expect("overflow when subtracting durations")
        }
    *)
    Definition sub (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "core::time::Duration" ],
              "expect",
              []
            |),
            [
              M.call_closure (|
                M.get_associated_function (| Ty.path "core::time::Duration", "checked_sub", [] |),
                [ M.read (| self |); M.read (| rhs |) ]
              |);
              M.read (| Value.String "overflow when subtracting durations" |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::ops::arith::Sub"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("Output", InstanceField.Ty _Output); ("sub", InstanceField.Method sub) ].
  End Impl_core_ops_arith_Sub_for_core_time_Duration.
  
  Module Impl_core_ops_arith_SubAssign_for_core_time_Duration.
    Definition Self : Ty.t := Ty.path "core::time::Duration".
    
    (*
        fn sub_assign(&mut self, rhs: Duration) {
            *self = *self - rhs;
        }
    *)
    Definition sub_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.read (|
            let~ _ :=
              M.write (|
                M.read (| self |),
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::arith::Sub",
                    Ty.path "core::time::Duration",
                    [ Ty.path "core::time::Duration" ],
                    "sub",
                    []
                  |),
                  [ M.read (| M.read (| self |) |); M.read (| rhs |) ]
                |)
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::ops::arith::SubAssign"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("sub_assign", InstanceField.Method sub_assign) ].
  End Impl_core_ops_arith_SubAssign_for_core_time_Duration.
  
  Module Impl_core_ops_arith_Mul_u32_for_core_time_Duration.
    Definition Self : Ty.t := Ty.path "core::time::Duration".
    
    (*     type Output = Duration; *)
    Definition _Output : Ty.t := Ty.path "core::time::Duration".
    
    (*
        fn mul(self, rhs: u32) -> Duration {
            self.checked_mul(rhs).expect("overflow when multiplying duration by scalar")
        }
    *)
    Definition mul (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "core::time::Duration" ],
              "expect",
              []
            |),
            [
              M.call_closure (|
                M.get_associated_function (| Ty.path "core::time::Duration", "checked_mul", [] |),
                [ M.read (| self |); M.read (| rhs |) ]
              |);
              M.read (| Value.String "overflow when multiplying duration by scalar" |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::ops::arith::Mul"
        Self
        (* Trait polymorphic types *) [ (* Rhs *) Ty.path "u32" ]
        (* Instance *) [ ("Output", InstanceField.Ty _Output); ("mul", InstanceField.Method mul) ].
  End Impl_core_ops_arith_Mul_u32_for_core_time_Duration.
  
  Module Impl_core_ops_arith_Mul_core_time_Duration_for_u32.
    Definition Self : Ty.t := Ty.path "u32".
    
    (*     type Output = Duration; *)
    Definition _Output : Ty.t := Ty.path "core::time::Duration".
    
    (*
        fn mul(self, rhs: Duration) -> Duration {
            rhs * self
        }
    *)
    Definition mul (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::ops::arith::Mul",
              Ty.path "core::time::Duration",
              [ Ty.path "u32" ],
              "mul",
              []
            |),
            [ M.read (| rhs |); M.read (| self |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::ops::arith::Mul"
        Self
        (* Trait polymorphic types *) [ (* Rhs *) Ty.path "core::time::Duration" ]
        (* Instance *) [ ("Output", InstanceField.Ty _Output); ("mul", InstanceField.Method mul) ].
  End Impl_core_ops_arith_Mul_core_time_Duration_for_u32.
  
  Module Impl_core_ops_arith_MulAssign_u32_for_core_time_Duration.
    Definition Self : Ty.t := Ty.path "core::time::Duration".
    
    (*
        fn mul_assign(&mut self, rhs: u32) {
            *self = *self * rhs;
        }
    *)
    Definition mul_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.read (|
            let~ _ :=
              M.write (|
                M.read (| self |),
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::arith::Mul",
                    Ty.path "core::time::Duration",
                    [ Ty.path "u32" ],
                    "mul",
                    []
                  |),
                  [ M.read (| M.read (| self |) |); M.read (| rhs |) ]
                |)
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::ops::arith::MulAssign"
        Self
        (* Trait polymorphic types *) [ (* Rhs *) Ty.path "u32" ]
        (* Instance *) [ ("mul_assign", InstanceField.Method mul_assign) ].
  End Impl_core_ops_arith_MulAssign_u32_for_core_time_Duration.
  
  Module Impl_core_ops_arith_Div_u32_for_core_time_Duration.
    Definition Self : Ty.t := Ty.path "core::time::Duration".
    
    (*     type Output = Duration; *)
    Definition _Output : Ty.t := Ty.path "core::time::Duration".
    
    (*
        fn div(self, rhs: u32) -> Duration {
            self.checked_div(rhs).expect("divide by zero error when dividing duration by scalar")
        }
    *)
    Definition div (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "core::time::Duration" ],
              "expect",
              []
            |),
            [
              M.call_closure (|
                M.get_associated_function (| Ty.path "core::time::Duration", "checked_div", [] |),
                [ M.read (| self |); M.read (| rhs |) ]
              |);
              M.read (| Value.String "divide by zero error when dividing duration by scalar" |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::ops::arith::Div"
        Self
        (* Trait polymorphic types *) [ (* Rhs *) Ty.path "u32" ]
        (* Instance *) [ ("Output", InstanceField.Ty _Output); ("div", InstanceField.Method div) ].
  End Impl_core_ops_arith_Div_u32_for_core_time_Duration.
  
  Module Impl_core_ops_arith_DivAssign_u32_for_core_time_Duration.
    Definition Self : Ty.t := Ty.path "core::time::Duration".
    
    (*
        fn div_assign(&mut self, rhs: u32) {
            *self = *self / rhs;
        }
    *)
    Definition div_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.read (|
            let~ _ :=
              M.write (|
                M.read (| self |),
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::arith::Div",
                    Ty.path "core::time::Duration",
                    [ Ty.path "u32" ],
                    "div",
                    []
                  |),
                  [ M.read (| M.read (| self |) |); M.read (| rhs |) ]
                |)
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::ops::arith::DivAssign"
        Self
        (* Trait polymorphic types *) [ (* Rhs *) Ty.path "u32" ]
        (* Instance *) [ ("div_assign", InstanceField.Method div_assign) ].
  End Impl_core_ops_arith_DivAssign_u32_for_core_time_Duration.
  
  Module Impl_core_iter_traits_accum_Sum_for_core_time_Duration.
    Definition Self : Ty.t := Ty.path "core::time::Duration".
    
    (*
        fn sum<I: Iterator<Item = Duration>>(iter: I) -> Duration {
            sum_durations!(iter)
        }
    *)
    Definition sum (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ _ as I ], [ iter ] =>
        ltac:(M.monadic
          (let iter := M.alloc (| iter |) in
          M.read (|
            let~ total_secs := M.alloc (| Value.Integer IntegerKind.U64 0 |) in
            let~ total_nanos := M.alloc (| Value.Integer IntegerKind.U64 0 |) in
            let~ _ :=
              M.use
                (M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::collect::IntoIterator",
                        I,
                        [],
                        "into_iter",
                        []
                      |),
                      [ M.read (| iter |) ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let iter := M.copy (| γ |) in
                        M.loop (|
                          ltac:(M.monadic
                            (let~ _ :=
                              M.match_operator (|
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::iter::traits::iterator::Iterator",
                                      I,
                                      [],
                                      "next",
                                      []
                                    |),
                                    [ iter ]
                                  |)
                                |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let _ :=
                                        M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                                      M.alloc (|
                                        M.never_to_any (| M.read (| M.break (||) |) |)
                                      |)));
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ0_0 :=
                                        M.SubPointer.get_struct_tuple_field (|
                                          γ,
                                          "core::option::Option::Some",
                                          0
                                        |) in
                                      let entry := M.copy (| γ0_0 |) in
                                      let~ _ :=
                                        M.write (|
                                          total_secs,
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply
                                                (Ty.path "core::option::Option")
                                                []
                                                [ Ty.path "u64" ],
                                              "expect",
                                              []
                                            |),
                                            [
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path "u64",
                                                  "checked_add",
                                                  []
                                                |),
                                                [
                                                  M.read (| total_secs |);
                                                  M.read (|
                                                    M.SubPointer.get_struct_record_field (|
                                                      entry,
                                                      "core::time::Duration",
                                                      "secs"
                                                    |)
                                                  |)
                                                ]
                                              |);
                                              M.read (|
                                                Value.String "overflow in iter::sum over durations"
                                              |)
                                            ]
                                          |)
                                        |) in
                                      let~ _ :=
                                        M.write (|
                                          total_nanos,
                                          M.read (|
                                            M.match_operator (|
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.path "u64",
                                                    "checked_add",
                                                    []
                                                  |),
                                                  [
                                                    M.read (| total_nanos |);
                                                    M.rust_cast
                                                      (M.read (|
                                                        M.SubPointer.get_struct_tuple_field (|
                                                          M.SubPointer.get_struct_record_field (|
                                                            entry,
                                                            "core::time::Duration",
                                                            "nanos"
                                                          |),
                                                          "core::time::Nanoseconds",
                                                          0
                                                        |)
                                                      |))
                                                  ]
                                                |)
                                              |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let γ0_0 :=
                                                      M.SubPointer.get_struct_tuple_field (|
                                                        γ,
                                                        "core::option::Option::Some",
                                                        0
                                                      |) in
                                                    let n := M.copy (| γ0_0 |) in
                                                    n));
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let _ :=
                                                      M.is_struct_tuple (|
                                                        γ,
                                                        "core::option::Option::None"
                                                      |) in
                                                    let~ _ :=
                                                      M.write (|
                                                        total_secs,
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.apply
                                                              (Ty.path "core::option::Option")
                                                              []
                                                              [ Ty.path "u64" ],
                                                            "expect",
                                                            []
                                                          |),
                                                          [
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.path "u64",
                                                                "checked_add",
                                                                []
                                                              |),
                                                              [
                                                                M.read (| total_secs |);
                                                                BinOp.Wrap.div (|
                                                                  M.read (| total_nanos |),
                                                                  M.rust_cast
                                                                    (M.read (|
                                                                      M.get_constant (|
                                                                        "core::time::NANOS_PER_SEC"
                                                                      |)
                                                                    |))
                                                                |)
                                                              ]
                                                            |);
                                                            M.read (|
                                                              Value.String
                                                                "overflow in iter::sum over durations"
                                                            |)
                                                          ]
                                                        |)
                                                      |) in
                                                    M.alloc (|
                                                      BinOp.Wrap.add (|
                                                        BinOp.Wrap.rem (|
                                                          M.read (| total_nanos |),
                                                          M.rust_cast
                                                            (M.read (|
                                                              M.get_constant (|
                                                                "core::time::NANOS_PER_SEC"
                                                              |)
                                                            |))
                                                        |),
                                                        M.rust_cast
                                                          (M.read (|
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              M.SubPointer.get_struct_record_field (|
                                                                entry,
                                                                "core::time::Duration",
                                                                "nanos"
                                                              |),
                                                              "core::time::Nanoseconds",
                                                              0
                                                            |)
                                                          |))
                                                      |)
                                                    |)))
                                              ]
                                            |)
                                          |)
                                        |) in
                                      M.alloc (| Value.Tuple [] |)))
                                ]
                              |) in
                            M.alloc (| Value.Tuple [] |)))
                        |)))
                  ]
                |)) in
            let~ _ :=
              M.write (|
                total_secs,
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u64" ],
                    "expect",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "u64", "checked_add", [] |),
                      [
                        M.read (| total_secs |);
                        BinOp.Wrap.div (|
                          M.read (| total_nanos |),
                          M.rust_cast
                            (M.read (| M.get_constant (| "core::time::NANOS_PER_SEC" |) |))
                        |)
                      ]
                    |);
                    M.read (| Value.String "overflow in iter::sum over durations" |)
                  ]
                |)
              |) in
            let~ _ :=
              M.write (|
                total_nanos,
                BinOp.Wrap.rem (|
                  M.read (| total_nanos |),
                  M.rust_cast (M.read (| M.get_constant (| "core::time::NANOS_PER_SEC" |) |))
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "core::time::Duration", "new", [] |),
                [ M.read (| total_secs |); M.rust_cast (M.read (| total_nanos |)) ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::iter::traits::accum::Sum"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("sum", InstanceField.Method sum) ].
  End Impl_core_iter_traits_accum_Sum_for_core_time_Duration.
  
  Module Impl_core_iter_traits_accum_Sum_ref__core_time_Duration_for_core_time_Duration.
    Definition Self : Ty.t := Ty.path "core::time::Duration".
    
    (*
        fn sum<I: Iterator<Item = &'a Duration>>(iter: I) -> Duration {
            sum_durations!(iter)
        }
    *)
    Definition sum (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ _ as I ], [ iter ] =>
        ltac:(M.monadic
          (let iter := M.alloc (| iter |) in
          M.read (|
            let~ total_secs := M.alloc (| Value.Integer IntegerKind.U64 0 |) in
            let~ total_nanos := M.alloc (| Value.Integer IntegerKind.U64 0 |) in
            let~ _ :=
              M.use
                (M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::collect::IntoIterator",
                        I,
                        [],
                        "into_iter",
                        []
                      |),
                      [ M.read (| iter |) ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let iter := M.copy (| γ |) in
                        M.loop (|
                          ltac:(M.monadic
                            (let~ _ :=
                              M.match_operator (|
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::iter::traits::iterator::Iterator",
                                      I,
                                      [],
                                      "next",
                                      []
                                    |),
                                    [ iter ]
                                  |)
                                |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let _ :=
                                        M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                                      M.alloc (|
                                        M.never_to_any (| M.read (| M.break (||) |) |)
                                      |)));
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ0_0 :=
                                        M.SubPointer.get_struct_tuple_field (|
                                          γ,
                                          "core::option::Option::Some",
                                          0
                                        |) in
                                      let entry := M.copy (| γ0_0 |) in
                                      let~ _ :=
                                        M.write (|
                                          total_secs,
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply
                                                (Ty.path "core::option::Option")
                                                []
                                                [ Ty.path "u64" ],
                                              "expect",
                                              []
                                            |),
                                            [
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path "u64",
                                                  "checked_add",
                                                  []
                                                |),
                                                [
                                                  M.read (| total_secs |);
                                                  M.read (|
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| entry |),
                                                      "core::time::Duration",
                                                      "secs"
                                                    |)
                                                  |)
                                                ]
                                              |);
                                              M.read (|
                                                Value.String "overflow in iter::sum over durations"
                                              |)
                                            ]
                                          |)
                                        |) in
                                      let~ _ :=
                                        M.write (|
                                          total_nanos,
                                          M.read (|
                                            M.match_operator (|
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.path "u64",
                                                    "checked_add",
                                                    []
                                                  |),
                                                  [
                                                    M.read (| total_nanos |);
                                                    M.rust_cast
                                                      (M.read (|
                                                        M.SubPointer.get_struct_tuple_field (|
                                                          M.SubPointer.get_struct_record_field (|
                                                            M.read (| entry |),
                                                            "core::time::Duration",
                                                            "nanos"
                                                          |),
                                                          "core::time::Nanoseconds",
                                                          0
                                                        |)
                                                      |))
                                                  ]
                                                |)
                                              |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let γ0_0 :=
                                                      M.SubPointer.get_struct_tuple_field (|
                                                        γ,
                                                        "core::option::Option::Some",
                                                        0
                                                      |) in
                                                    let n := M.copy (| γ0_0 |) in
                                                    n));
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let _ :=
                                                      M.is_struct_tuple (|
                                                        γ,
                                                        "core::option::Option::None"
                                                      |) in
                                                    let~ _ :=
                                                      M.write (|
                                                        total_secs,
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.apply
                                                              (Ty.path "core::option::Option")
                                                              []
                                                              [ Ty.path "u64" ],
                                                            "expect",
                                                            []
                                                          |),
                                                          [
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.path "u64",
                                                                "checked_add",
                                                                []
                                                              |),
                                                              [
                                                                M.read (| total_secs |);
                                                                BinOp.Wrap.div (|
                                                                  M.read (| total_nanos |),
                                                                  M.rust_cast
                                                                    (M.read (|
                                                                      M.get_constant (|
                                                                        "core::time::NANOS_PER_SEC"
                                                                      |)
                                                                    |))
                                                                |)
                                                              ]
                                                            |);
                                                            M.read (|
                                                              Value.String
                                                                "overflow in iter::sum over durations"
                                                            |)
                                                          ]
                                                        |)
                                                      |) in
                                                    M.alloc (|
                                                      BinOp.Wrap.add (|
                                                        BinOp.Wrap.rem (|
                                                          M.read (| total_nanos |),
                                                          M.rust_cast
                                                            (M.read (|
                                                              M.get_constant (|
                                                                "core::time::NANOS_PER_SEC"
                                                              |)
                                                            |))
                                                        |),
                                                        M.rust_cast
                                                          (M.read (|
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              M.SubPointer.get_struct_record_field (|
                                                                M.read (| entry |),
                                                                "core::time::Duration",
                                                                "nanos"
                                                              |),
                                                              "core::time::Nanoseconds",
                                                              0
                                                            |)
                                                          |))
                                                      |)
                                                    |)))
                                              ]
                                            |)
                                          |)
                                        |) in
                                      M.alloc (| Value.Tuple [] |)))
                                ]
                              |) in
                            M.alloc (| Value.Tuple [] |)))
                        |)))
                  ]
                |)) in
            let~ _ :=
              M.write (|
                total_secs,
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u64" ],
                    "expect",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "u64", "checked_add", [] |),
                      [
                        M.read (| total_secs |);
                        BinOp.Wrap.div (|
                          M.read (| total_nanos |),
                          M.rust_cast
                            (M.read (| M.get_constant (| "core::time::NANOS_PER_SEC" |) |))
                        |)
                      ]
                    |);
                    M.read (| Value.String "overflow in iter::sum over durations" |)
                  ]
                |)
              |) in
            let~ _ :=
              M.write (|
                total_nanos,
                BinOp.Wrap.rem (|
                  M.read (| total_nanos |),
                  M.rust_cast (M.read (| M.get_constant (| "core::time::NANOS_PER_SEC" |) |))
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "core::time::Duration", "new", [] |),
                [ M.read (| total_secs |); M.rust_cast (M.read (| total_nanos |)) ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::iter::traits::accum::Sum"
        Self
        (* Trait polymorphic types *)
        [ (* A *) Ty.apply (Ty.path "&") [] [ Ty.path "core::time::Duration" ] ]
        (* Instance *) [ ("sum", InstanceField.Method sum) ].
  End Impl_core_iter_traits_accum_Sum_ref__core_time_Duration_for_core_time_Duration.
  
  Module Impl_core_fmt_Debug_for_core_time_Duration.
    Definition Self : Ty.t := Ty.path "core::time::Duration".
    
    (*
        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
            /// Formats a floating point number in decimal notation.
            ///
            /// The number is given as the `integer_part` and a fractional part.
            /// The value of the fractional part is `fractional_part / divisor`. So
            /// `integer_part` = 3, `fractional_part` = 12 and `divisor` = 100
            /// represents the number `3.012`. Trailing zeros are omitted.
            ///
            /// `divisor` must not be above 100_000_000. It also should be a power
            /// of 10, everything else doesn't make sense. `fractional_part` has
            /// to be less than `10 * divisor`!
            ///
            /// A prefix and postfix may be added. The whole thing is padded
            /// to the formatter's `width`, if specified.
            fn fmt_decimal(
                f: &mut fmt::Formatter<'_>,
                integer_part: u64,
                mut fractional_part: u32,
                mut divisor: u32,
                prefix: &str,
                postfix: &str,
            ) -> fmt::Result {
                // Encode the fractional part into a temporary buffer. The buffer
                // only need to hold 9 elements, because `fractional_part` has to
                // be smaller than 10^9. The buffer is prefilled with '0' digits
                // to simplify the code below.
                let mut buf = [b'0'; 9];
    
                // The next digit is written at this position
                let mut pos = 0;
    
                // We keep writing digits into the buffer while there are non-zero
                // digits left and we haven't written enough digits yet.
                while fractional_part > 0 && pos < f.precision().unwrap_or(9) {
                    // Write new digit into the buffer
                    buf[pos] = b'0' + (fractional_part / divisor) as u8;
    
                    fractional_part %= divisor;
                    divisor /= 10;
                    pos += 1;
                }
    
                // If a precision < 9 was specified, there may be some non-zero
                // digits left that weren't written into the buffer. In that case we
                // need to perform rounding to match the semantics of printing
                // normal floating point numbers. However, we only need to do work
                // when rounding up. This happens if the first digit of the
                // remaining ones is >= 5.
                let integer_part = if fractional_part > 0 && fractional_part >= divisor * 5 {
                    // Round up the number contained in the buffer. We go through
                    // the buffer backwards and keep track of the carry.
                    let mut rev_pos = pos;
                    let mut carry = true;
                    while carry && rev_pos > 0 {
                        rev_pos -= 1;
    
                        // If the digit in the buffer is not '9', we just need to
                        // increment it and can stop then (since we don't have a
                        // carry anymore). Otherwise, we set it to '0' (overflow)
                        // and continue.
                        if buf[rev_pos] < b'9' {
                            buf[rev_pos] += 1;
                            carry = false;
                        } else {
                            buf[rev_pos] = b'0';
                        }
                    }
    
                    // If we still have the carry bit set, that means that we set
                    // the whole buffer to '0's and need to increment the integer
                    // part.
                    if carry {
                        // If `integer_part == u64::MAX` and precision < 9, any
                        // carry of the overflow during rounding of the
                        // `fractional_part` into the `integer_part` will cause the
                        // `integer_part` itself to overflow. Avoid this by using an
                        // `Option<u64>`, with `None` representing `u64::MAX + 1`.
                        integer_part.checked_add(1)
                    } else {
                        Some(integer_part)
                    }
                } else {
                    Some(integer_part)
                };
    
                // Determine the end of the buffer: if precision is set, we just
                // use as many digits from the buffer (capped to 9). If it isn't
                // set, we only use all digits up to the last non-zero one.
                let end = f.precision().map(|p| crate::cmp::min(p, 9)).unwrap_or(pos);
    
                // This closure emits the formatted duration without emitting any
                // padding (padding is calculated below).
                let emit_without_padding = |f: &mut fmt::Formatter<'_>| {
                    if let Some(integer_part) = integer_part {
                        write!(f, "{}{}", prefix, integer_part)?;
                    } else {
                        // u64::MAX + 1 == 18446744073709551616
                        write!(f, "{}18446744073709551616", prefix)?;
                    }
    
                    // Write the decimal point and the fractional part (if any).
                    if end > 0 {
                        // SAFETY: We are only writing ASCII digits into the buffer and
                        // it was initialized with '0's, so it contains valid UTF8.
                        let s = unsafe { crate::str::from_utf8_unchecked(&buf[..end]) };
    
                        // If the user request a precision > 9, we pad '0's at the end.
                        let w = f.precision().unwrap_or(pos);
                        write!(f, ".{:0<width$}", s, width = w)?;
                    }
    
                    write!(f, "{}", postfix)
                };
    
                match f.width() {
                    None => {
                        // No `width` specified. There's no need to calculate the
                        // length of the output in this case, just emit it.
                        emit_without_padding(f)
                    }
                    Some(requested_w) => {
                        // A `width` was specified. Calculate the actual width of
                        // the output in order to calculate the required padding.
                        // It consists of 4 parts:
                        // 1. The prefix: is either "+" or "", so we can just use len().
                        // 2. The postfix: can be "µs" so we have to count UTF8 characters.
                        let mut actual_w = prefix.len() + postfix.chars().count();
                        // 3. The integer part:
                        if let Some(integer_part) = integer_part {
                            if let Some(log) = integer_part.checked_ilog10() {
                                // integer_part is > 0, so has length log10(x)+1
                                actual_w += 1 + log as usize;
                            } else {
                                // integer_part is 0, so has length 1.
                                actual_w += 1;
                            }
                        } else {
                            // integer_part is u64::MAX + 1, so has length 20
                            actual_w += 20;
                        }
                        // 4. The fractional part (if any):
                        if end > 0 {
                            let frac_part_w = f.precision().unwrap_or(pos);
                            actual_w += 1 + frac_part_w;
                        }
    
                        if requested_w <= actual_w {
                            // Output is already longer than `width`, so don't pad.
                            emit_without_padding(f)
                        } else {
                            // We need to add padding. Use the `Formatter::padding` helper function.
                            let default_align = fmt::Alignment::Left;
                            let post_padding = f.padding(requested_w - actual_w, default_align)?;
                            emit_without_padding(f)?;
                            post_padding.write(f)
                        }
                    }
                }
            }
    
            // Print leading '+' sign if requested
            let prefix = if f.sign_plus() { "+" } else { "" };
    
            if self.secs > 0 {
                fmt_decimal(f, self.secs, self.nanos.0, NANOS_PER_SEC / 10, prefix, "s")
            } else if self.nanos.0 >= NANOS_PER_MILLI {
                fmt_decimal(
                    f,
                    (self.nanos.0 / NANOS_PER_MILLI) as u64,
                    self.nanos.0 % NANOS_PER_MILLI,
                    NANOS_PER_MILLI / 10,
                    prefix,
                    "ms",
                )
            } else if self.nanos.0 >= NANOS_PER_MICRO {
                fmt_decimal(
                    f,
                    (self.nanos.0 / NANOS_PER_MICRO) as u64,
                    self.nanos.0 % NANOS_PER_MICRO,
                    NANOS_PER_MICRO / 10,
                    prefix,
                    "µs",
                )
            } else {
                fmt_decimal(f, self.nanos.0 as u64, 0, 1, prefix, "ns")
            }
        }
    *)
    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 (|
            let~ prefix :=
              M.copy (|
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::Formatter",
                                  "sign_plus",
                                  []
                                |),
                                [ M.read (| f |) ]
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        Value.String "+"));
                    fun γ => ltac:(M.monadic (M.alloc (| M.read (| Value.String "" |) |)))
                  ]
                |)
              |) in
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          BinOp.gt (|
                            M.read (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::time::Duration",
                                "secs"
                              |)
                            |),
                            Value.Integer IntegerKind.U64 0
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (| Self, "fmt_decimal.fmt", [] |),
                        [
                          M.read (| f |);
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "core::time::Duration",
                              "secs"
                            |)
                          |);
                          M.read (|
                            M.SubPointer.get_struct_tuple_field (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::time::Duration",
                                "nanos"
                              |),
                              "core::time::Nanoseconds",
                              0
                            |)
                          |);
                          BinOp.Wrap.div (|
                            M.read (| M.get_constant (| "core::time::NANOS_PER_SEC" |) |),
                            Value.Integer IntegerKind.U32 10
                          |);
                          M.read (| prefix |);
                          M.read (| Value.String "s" |)
                        ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  BinOp.ge (|
                                    M.read (|
                                      M.SubPointer.get_struct_tuple_field (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "core::time::Duration",
                                          "nanos"
                                        |),
                                        "core::time::Nanoseconds",
                                        0
                                      |)
                                    |),
                                    M.read (| M.get_constant (| "core::time::NANOS_PER_MILLI" |) |)
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (| Self, "fmt_decimal.fmt", [] |),
                                [
                                  M.read (| f |);
                                  M.rust_cast
                                    (BinOp.Wrap.div (|
                                      M.read (|
                                        M.SubPointer.get_struct_tuple_field (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "core::time::Duration",
                                            "nanos"
                                          |),
                                          "core::time::Nanoseconds",
                                          0
                                        |)
                                      |),
                                      M.read (|
                                        M.get_constant (| "core::time::NANOS_PER_MILLI" |)
                                      |)
                                    |));
                                  BinOp.Wrap.rem (|
                                    M.read (|
                                      M.SubPointer.get_struct_tuple_field (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "core::time::Duration",
                                          "nanos"
                                        |),
                                        "core::time::Nanoseconds",
                                        0
                                      |)
                                    |),
                                    M.read (| M.get_constant (| "core::time::NANOS_PER_MILLI" |) |)
                                  |);
                                  BinOp.Wrap.div (|
                                    M.read (| M.get_constant (| "core::time::NANOS_PER_MILLI" |) |),
                                    Value.Integer IntegerKind.U32 10
                                  |);
                                  M.read (| prefix |);
                                  M.read (| Value.String "ms" |)
                                ]
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          BinOp.ge (|
                                            M.read (|
                                              M.SubPointer.get_struct_tuple_field (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| self |),
                                                  "core::time::Duration",
                                                  "nanos"
                                                |),
                                                "core::time::Nanoseconds",
                                                0
                                              |)
                                            |),
                                            M.read (|
                                              M.get_constant (| "core::time::NANOS_PER_MICRO" |)
                                            |)
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (| Self, "fmt_decimal.fmt", [] |),
                                        [
                                          M.read (| f |);
                                          M.rust_cast
                                            (BinOp.Wrap.div (|
                                              M.read (|
                                                M.SubPointer.get_struct_tuple_field (|
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.read (| self |),
                                                    "core::time::Duration",
                                                    "nanos"
                                                  |),
                                                  "core::time::Nanoseconds",
                                                  0
                                                |)
                                              |),
                                              M.read (|
                                                M.get_constant (| "core::time::NANOS_PER_MICRO" |)
                                              |)
                                            |));
                                          BinOp.Wrap.rem (|
                                            M.read (|
                                              M.SubPointer.get_struct_tuple_field (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| self |),
                                                  "core::time::Duration",
                                                  "nanos"
                                                |),
                                                "core::time::Nanoseconds",
                                                0
                                              |)
                                            |),
                                            M.read (|
                                              M.get_constant (| "core::time::NANOS_PER_MICRO" |)
                                            |)
                                          |);
                                          BinOp.Wrap.div (|
                                            M.read (|
                                              M.get_constant (| "core::time::NANOS_PER_MICRO" |)
                                            |),
                                            Value.Integer IntegerKind.U32 10
                                          |);
                                          M.read (| prefix |);
                                          M.read (| Value.String (String.String "181" "s") |)
                                        ]
                                      |)
                                    |)));
                                fun γ =>
                                  ltac:(M.monadic
                                    (M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (| Self, "fmt_decimal.fmt", [] |),
                                        [
                                          M.read (| f |);
                                          M.rust_cast
                                            (M.read (|
                                              M.SubPointer.get_struct_tuple_field (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| self |),
                                                  "core::time::Duration",
                                                  "nanos"
                                                |),
                                                "core::time::Nanoseconds",
                                                0
                                              |)
                                            |));
                                          Value.Integer IntegerKind.U32 0;
                                          Value.Integer IntegerKind.U32 1;
                                          M.read (| prefix |);
                                          M.read (| Value.String "ns" |)
                                        ]
                                      |)
                                    |)))
                              ]
                            |)))
                      ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => 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_time_Duration.
  
  (* StructRecord
    {
      name := "TryFromFloatSecsError";
      const_params := [];
      ty_params := [];
      fields := [ ("kind", Ty.path "core::time::TryFromFloatSecsErrorKind") ];
    } *)
  
  Module Impl_core_fmt_Debug_for_core_time_TryFromFloatSecsError.
    Definition Self : Ty.t := Ty.path "core::time::TryFromFloatSecsError".
    
    (* 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 "TryFromFloatSecsError" |);
              M.read (| Value.String "kind" |);
              M.alloc (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::time::TryFromFloatSecsError",
                  "kind"
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::fmt::Debug"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
  End Impl_core_fmt_Debug_for_core_time_TryFromFloatSecsError.
  
  Module Impl_core_clone_Clone_for_core_time_TryFromFloatSecsError.
    Definition Self : Ty.t := Ty.path "core::time::TryFromFloatSecsError".
    
    (* 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::time::TryFromFloatSecsError"
            [
              ("kind",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.path "core::time::TryFromFloatSecsErrorKind",
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::time::TryFromFloatSecsError",
                      "kind"
                    |)
                  ]
                |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::clone::Clone"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("clone", InstanceField.Method clone) ].
  End Impl_core_clone_Clone_for_core_time_TryFromFloatSecsError.
  
  Module Impl_core_marker_StructuralPartialEq_for_core_time_TryFromFloatSecsError.
    Definition Self : Ty.t := Ty.path "core::time::TryFromFloatSecsError".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_core_time_TryFromFloatSecsError.
  
  Module Impl_core_cmp_PartialEq_for_core_time_TryFromFloatSecsError.
    Definition Self : Ty.t := Ty.path "core::time::TryFromFloatSecsError".
    
    (* PartialEq *)
    Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::cmp::PartialEq",
              Ty.path "core::time::TryFromFloatSecsErrorKind",
              [ Ty.path "core::time::TryFromFloatSecsErrorKind" ],
              "eq",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::time::TryFromFloatSecsError",
                "kind"
              |);
              M.SubPointer.get_struct_record_field (|
                M.read (| other |),
                "core::time::TryFromFloatSecsError",
                "kind"
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::PartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("eq", InstanceField.Method eq) ].
  End Impl_core_cmp_PartialEq_for_core_time_TryFromFloatSecsError.
  
  Module Impl_core_cmp_Eq_for_core_time_TryFromFloatSecsError.
    Definition Self : Ty.t := Ty.path "core::time::TryFromFloatSecsError".
    
    (* Eq *)
    Definition assert_receiver_is_total_eq
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              Value.DeclaredButUndefined,
              [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::Eq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *)
        [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
  End Impl_core_cmp_Eq_for_core_time_TryFromFloatSecsError.
  
  Module Impl_core_time_TryFromFloatSecsError.
    Definition Self : Ty.t := Ty.path "core::time::TryFromFloatSecsError".
    
    (*
        const fn description(&self) -> &'static str {
            match self.kind {
                TryFromFloatSecsErrorKind::Negative => {
                    "cannot convert float seconds to Duration: value is negative"
                }
                TryFromFloatSecsErrorKind::OverflowOrNan => {
                    "cannot convert float seconds to Duration: value is either too big or NaN"
                }
            }
        }
    *)
    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 (|
            M.match_operator (|
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::time::TryFromFloatSecsError",
                "kind"
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "core::time::TryFromFloatSecsErrorKind::Negative"
                      |) in
                    Value.String "cannot convert float seconds to Duration: value is negative"));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "core::time::TryFromFloatSecsErrorKind::OverflowOrNan"
                      |) in
                    Value.String
                      "cannot convert float seconds to Duration: value is either too big or NaN"))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_description : M.IsAssociatedFunction Self "description" description.
  End Impl_core_time_TryFromFloatSecsError.
  
  Module Impl_core_fmt_Display_for_core_time_TryFromFloatSecsError.
    Definition Self : Ty.t := Ty.path "core::time::TryFromFloatSecsError".
    
    (*
        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
            self.description().fmt(f)
        }
    *)
    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_trait_method (| "core::fmt::Display", Ty.path "str", [], "fmt", [] |),
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "core::time::TryFromFloatSecsError",
                  "description",
                  []
                |),
                [ M.read (| self |) ]
              |);
              M.read (| f |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::fmt::Display"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
  End Impl_core_fmt_Display_for_core_time_TryFromFloatSecsError.
  
  (*
  Enum TryFromFloatSecsErrorKind
  {
    const_params := [];
    ty_params := [];
    variants :=
      [
        {
          name := "Negative";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "OverflowOrNan";
          item := StructTuple [];
          discriminant := None;
        }
      ];
  }
  *)
  
  Module Impl_core_fmt_Debug_for_core_time_TryFromFloatSecsErrorKind.
    Definition Self : Ty.t := Ty.path "core::time::TryFromFloatSecsErrorKind".
    
    (* 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 (|
                M.match_operator (|
                  self,
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "core::time::TryFromFloatSecsErrorKind::Negative"
                          |) in
                        M.alloc (| M.read (| Value.String "Negative" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "core::time::TryFromFloatSecsErrorKind::OverflowOrNan"
                          |) in
                        M.alloc (| M.read (| Value.String "OverflowOrNan" |) |)))
                  ]
                |)
              |)
            ]
          |)))
      | _, _, _ => 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_time_TryFromFloatSecsErrorKind.
  
  Module Impl_core_clone_Clone_for_core_time_TryFromFloatSecsErrorKind.
    Definition Self : Ty.t := Ty.path "core::time::TryFromFloatSecsErrorKind".
    
    (* Clone *)
    Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "core::time::TryFromFloatSecsErrorKind::Negative"
                      |) in
                    M.alloc (|
                      Value.StructTuple "core::time::TryFromFloatSecsErrorKind::Negative" []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "core::time::TryFromFloatSecsErrorKind::OverflowOrNan"
                      |) in
                    M.alloc (|
                      Value.StructTuple "core::time::TryFromFloatSecsErrorKind::OverflowOrNan" []
                    |)))
              ]
            |)
          |)))
      | _, _, _ => 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_time_TryFromFloatSecsErrorKind.
  
  Module Impl_core_marker_StructuralPartialEq_for_core_time_TryFromFloatSecsErrorKind.
    Definition Self : Ty.t := Ty.path "core::time::TryFromFloatSecsErrorKind".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_core_time_TryFromFloatSecsErrorKind.
  
  Module Impl_core_cmp_PartialEq_for_core_time_TryFromFloatSecsErrorKind.
    Definition Self : Ty.t := Ty.path "core::time::TryFromFloatSecsErrorKind".
    
    (* 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::time::TryFromFloatSecsErrorKind" ]
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            let~ __arg1_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "core::time::TryFromFloatSecsErrorKind" ]
                  |),
                  [ 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_time_TryFromFloatSecsErrorKind.
  
  Module Impl_core_cmp_Eq_for_core_time_TryFromFloatSecsErrorKind.
    Definition Self : Ty.t := Ty.path "core::time::TryFromFloatSecsErrorKind".
    
    (* 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_time_TryFromFloatSecsErrorKind.
  
End time.
