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

Module num.
  Module dec2flt.
    Module number.
      Definition value_INT_POW10 : Value.t :=
        M.run
          ltac:(M.monadic
            (M.alloc (|
              Value.Array
                [
                  Value.Integer IntegerKind.U64 1;
                  Value.Integer IntegerKind.U64 10;
                  Value.Integer IntegerKind.U64 100;
                  Value.Integer IntegerKind.U64 1000;
                  Value.Integer IntegerKind.U64 10000;
                  Value.Integer IntegerKind.U64 100000;
                  Value.Integer IntegerKind.U64 1000000;
                  Value.Integer IntegerKind.U64 10000000;
                  Value.Integer IntegerKind.U64 100000000;
                  Value.Integer IntegerKind.U64 1000000000;
                  Value.Integer IntegerKind.U64 10000000000;
                  Value.Integer IntegerKind.U64 100000000000;
                  Value.Integer IntegerKind.U64 1000000000000;
                  Value.Integer IntegerKind.U64 10000000000000;
                  Value.Integer IntegerKind.U64 100000000000000;
                  Value.Integer IntegerKind.U64 1000000000000000
                ]
            |))).
      
      (* StructRecord
        {
          name := "Number";
          const_params := [];
          ty_params := [];
          fields :=
            [
              ("exponent", Ty.path "i64");
              ("mantissa", Ty.path "u64");
              ("negative", Ty.path "bool");
              ("many_digits", Ty.path "bool")
            ];
        } *)
      
      Module Impl_core_clone_Clone_for_core_num_dec2flt_number_Number.
        Definition Self : Ty.t := Ty.path "core::num::dec2flt::number::Number".
        
        (* Clone *)
        Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.read (|
                M.match_operator (|
                  Value.DeclaredButUndefined,
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (M.match_operator (|
                          Value.DeclaredButUndefined,
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (M.match_operator (|
                                  Value.DeclaredButUndefined,
                                  [ fun γ => ltac:(M.monadic (M.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_num_dec2flt_number_Number.
      
      Module Impl_core_marker_Copy_for_core_num_dec2flt_number_Number.
        Definition Self : Ty.t := Ty.path "core::num::dec2flt::number::Number".
        
        Axiom Implements :
          M.IsTraitInstance
            "core::marker::Copy"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_marker_Copy_for_core_num_dec2flt_number_Number.
      
      Module Impl_core_fmt_Debug_for_core_num_dec2flt_number_Number.
        Definition Self : Ty.t := Ty.path "core::num::dec2flt::number::Number".
        
        (* 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_field4_finish",
                  []
                |),
                [
                  M.read (| f |);
                  M.read (| Value.String "Number" |);
                  M.read (| Value.String "exponent" |);
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::num::dec2flt::number::Number",
                    "exponent"
                  |);
                  M.read (| Value.String "mantissa" |);
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::num::dec2flt::number::Number",
                    "mantissa"
                  |);
                  M.read (| Value.String "negative" |);
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::num::dec2flt::number::Number",
                    "negative"
                  |);
                  M.read (| Value.String "many_digits" |);
                  M.alloc (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::num::dec2flt::number::Number",
                      "many_digits"
                    |)
                  |)
                ]
              |)))
          | _, _, _ => 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_num_dec2flt_number_Number.
      
      Module Impl_core_default_Default_for_core_num_dec2flt_number_Number.
        Definition Self : Ty.t := Ty.path "core::num::dec2flt::number::Number".
        
        (* Default *)
        Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [] =>
            ltac:(M.monadic
              (Value.StructRecord
                "core::num::dec2flt::number::Number"
                [
                  ("exponent",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::default::Default",
                        Ty.path "i64",
                        [],
                        "default",
                        []
                      |),
                      []
                    |));
                  ("mantissa",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::default::Default",
                        Ty.path "u64",
                        [],
                        "default",
                        []
                      |),
                      []
                    |));
                  ("negative",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::default::Default",
                        Ty.path "bool",
                        [],
                        "default",
                        []
                      |),
                      []
                    |));
                  ("many_digits",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::default::Default",
                        Ty.path "bool",
                        [],
                        "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_num_dec2flt_number_Number.
      
      Module Impl_core_marker_StructuralPartialEq_for_core_num_dec2flt_number_Number.
        Definition Self : Ty.t := Ty.path "core::num::dec2flt::number::Number".
        
        Axiom Implements :
          M.IsTraitInstance
            "core::marker::StructuralPartialEq"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_marker_StructuralPartialEq_for_core_num_dec2flt_number_Number.
      
      Module Impl_core_cmp_PartialEq_for_core_num_dec2flt_number_Number.
        Definition Self : Ty.t := Ty.path "core::num::dec2flt::number::Number".
        
        (* 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 (|
                LogicalOp.and (|
                  LogicalOp.and (|
                    BinOp.eq (|
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::num::dec2flt::number::Number",
                          "exponent"
                        |)
                      |),
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| other |),
                          "core::num::dec2flt::number::Number",
                          "exponent"
                        |)
                      |)
                    |),
                    ltac:(M.monadic
                      (BinOp.eq (|
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "core::num::dec2flt::number::Number",
                            "mantissa"
                          |)
                        |),
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| other |),
                            "core::num::dec2flt::number::Number",
                            "mantissa"
                          |)
                        |)
                      |)))
                  |),
                  ltac:(M.monadic
                    (BinOp.eq (|
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::num::dec2flt::number::Number",
                          "negative"
                        |)
                      |),
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| other |),
                          "core::num::dec2flt::number::Number",
                          "negative"
                        |)
                      |)
                    |)))
                |),
                ltac:(M.monadic
                  (BinOp.eq (|
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::num::dec2flt::number::Number",
                        "many_digits"
                      |)
                    |),
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| other |),
                        "core::num::dec2flt::number::Number",
                        "many_digits"
                      |)
                    |)
                  |)))
              |)))
          | _, _, _ => 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_num_dec2flt_number_Number.
      
      Module Impl_core_cmp_Eq_for_core_num_dec2flt_number_Number.
        Definition Self : Ty.t := Ty.path "core::num::dec2flt::number::Number".
        
        (* 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.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_num_dec2flt_number_Number.
      
      Module Impl_core_num_dec2flt_number_Number.
        Definition Self : Ty.t := Ty.path "core::num::dec2flt::number::Number".
        
        (*
            fn is_fast_path<F: RawFloat>(&self) -> bool {
                F::MIN_EXPONENT_FAST_PATH <= self.exponent
                    && self.exponent <= F::MAX_EXPONENT_DISGUISED_FAST_PATH
                    && self.mantissa <= F::MAX_MANTISSA_FAST_PATH
                    && !self.many_digits
            }
        *)
        Definition is_fast_path (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ F ], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              LogicalOp.and (|
                LogicalOp.and (|
                  LogicalOp.and (|
                    BinOp.le (|
                      M.read (|
                        M.get_constant (|
                          "core::num::dec2flt::float::RawFloat::MIN_EXPONENT_FAST_PATH"
                        |)
                      |),
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::num::dec2flt::number::Number",
                          "exponent"
                        |)
                      |)
                    |),
                    ltac:(M.monadic
                      (BinOp.le (|
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "core::num::dec2flt::number::Number",
                            "exponent"
                          |)
                        |),
                        M.read (|
                          M.get_constant (|
                            "core::num::dec2flt::float::RawFloat::MAX_EXPONENT_DISGUISED_FAST_PATH"
                          |)
                        |)
                      |)))
                  |),
                  ltac:(M.monadic
                    (BinOp.le (|
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::num::dec2flt::number::Number",
                          "mantissa"
                        |)
                      |),
                      M.read (|
                        M.get_constant (|
                          "core::num::dec2flt::float::RawFloat::MAX_MANTISSA_FAST_PATH"
                        |)
                      |)
                    |)))
                |),
                ltac:(M.monadic
                  (UnOp.not (|
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::num::dec2flt::number::Number",
                        "many_digits"
                      |)
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_is_fast_path :
          M.IsAssociatedFunction Self "is_fast_path" is_fast_path.
        
        (*
            pub fn try_fast_path<F: RawFloat>(&self) -> Option<F> {
                // Here we need to work around <https://github.com/rust-lang/rust/issues/114479>.
                // The fast path crucially depends on arithmetic being rounded to the correct number of bits
                // without any intermediate rounding. On x86 (without SSE or SSE2) this requires the precision
                // of the x87 FPU stack to be changed so that it directly rounds to 64/32 bit.
                // The `set_precision` function takes care of setting the precision on architectures which
                // require setting it by changing the global state (like the control word of the x87 FPU).
                let _cw = set_precision::<F>();
        
                if self.is_fast_path::<F>() {
                    let mut value = if self.exponent <= F::MAX_EXPONENT_FAST_PATH {
                        // normal fast path
                        let value = F::from_u64(self.mantissa);
                        if self.exponent < 0 {
                            value / F::pow10_fast_path((-self.exponent) as _)
                        } else {
                            value * F::pow10_fast_path(self.exponent as _)
                        }
                    } else {
                        // disguised fast path
                        let shift = self.exponent - F::MAX_EXPONENT_FAST_PATH;
                        let mantissa = self.mantissa.checked_mul(INT_POW10[shift as usize])?;
                        if mantissa > F::MAX_MANTISSA_FAST_PATH {
                            return None;
                        }
                        F::from_u64(mantissa) * F::pow10_fast_path(F::MAX_EXPONENT_FAST_PATH as _)
                    };
                    if self.negative {
                        value = -value;
                    }
                    Some(value)
                } else {
                    None
                }
            }
        *)
        Definition try_fast_path (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ F ], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let~ _cw :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_function (|
                            "core::num::dec2flt::fpu::fpu_precision::set_precision",
                            [ F ]
                          |),
                          []
                        |)
                      |) in
                    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::num::dec2flt::number::Number",
                                      "is_fast_path",
                                      [ F ]
                                    |),
                                    [ M.read (| self |) ]
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            let~ value :=
                              M.copy (|
                                M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ :=
                                          M.use
                                            (M.alloc (|
                                              BinOp.le (|
                                                M.read (|
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.read (| self |),
                                                    "core::num::dec2flt::number::Number",
                                                    "exponent"
                                                  |)
                                                |),
                                                M.read (|
                                                  M.get_constant (|
                                                    "core::num::dec2flt::float::RawFloat::MAX_EXPONENT_FAST_PATH"
                                                  |)
                                                |)
                                              |)
                                            |)) in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        let~ value :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::num::dec2flt::float::RawFloat",
                                                F,
                                                [],
                                                "from_u64",
                                                []
                                              |),
                                              [
                                                M.read (|
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.read (| self |),
                                                    "core::num::dec2flt::number::Number",
                                                    "mantissa"
                                                  |)
                                                |)
                                              ]
                                            |)
                                          |) in
                                        M.match_operator (|
                                          M.alloc (| Value.Tuple [] |),
                                          [
                                            fun γ =>
                                              ltac:(M.monadic
                                                (let γ :=
                                                  M.use
                                                    (M.alloc (|
                                                      BinOp.lt (|
                                                        M.read (|
                                                          M.SubPointer.get_struct_record_field (|
                                                            M.read (| self |),
                                                            "core::num::dec2flt::number::Number",
                                                            "exponent"
                                                          |)
                                                        |),
                                                        Value.Integer IntegerKind.I64 0
                                                      |)
                                                    |)) in
                                                let _ :=
                                                  M.is_constant_or_break_match (|
                                                    M.read (| γ |),
                                                    Value.Bool true
                                                  |) in
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::ops::arith::Div",
                                                      F,
                                                      [ F ],
                                                      "div",
                                                      []
                                                    |),
                                                    [
                                                      M.read (| value |);
                                                      M.call_closure (|
                                                        M.get_trait_method (|
                                                          "core::num::dec2flt::float::RawFloat",
                                                          F,
                                                          [],
                                                          "pow10_fast_path",
                                                          []
                                                        |),
                                                        [
                                                          M.rust_cast
                                                            (UnOp.neg (|
                                                              M.read (|
                                                                M.SubPointer.get_struct_record_field (|
                                                                  M.read (| self |),
                                                                  "core::num::dec2flt::number::Number",
                                                                  "exponent"
                                                                |)
                                                              |)
                                                            |))
                                                        ]
                                                      |)
                                                    ]
                                                  |)
                                                |)));
                                            fun γ =>
                                              ltac:(M.monadic
                                                (M.alloc (|
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::ops::arith::Mul",
                                                      F,
                                                      [ F ],
                                                      "mul",
                                                      []
                                                    |),
                                                    [
                                                      M.read (| value |);
                                                      M.call_closure (|
                                                        M.get_trait_method (|
                                                          "core::num::dec2flt::float::RawFloat",
                                                          F,
                                                          [],
                                                          "pow10_fast_path",
                                                          []
                                                        |),
                                                        [
                                                          M.rust_cast
                                                            (M.read (|
                                                              M.SubPointer.get_struct_record_field (|
                                                                M.read (| self |),
                                                                "core::num::dec2flt::number::Number",
                                                                "exponent"
                                                              |)
                                                            |))
                                                        ]
                                                      |)
                                                    ]
                                                  |)
                                                |)))
                                          ]
                                        |)));
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let~ shift :=
                                          M.alloc (|
                                            BinOp.Wrap.sub (|
                                              M.read (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| self |),
                                                  "core::num::dec2flt::number::Number",
                                                  "exponent"
                                                |)
                                              |),
                                              M.read (|
                                                M.get_constant (|
                                                  "core::num::dec2flt::float::RawFloat::MAX_EXPONENT_FAST_PATH"
                                                |)
                                              |)
                                            |)
                                          |) in
                                        let~ mantissa :=
                                          M.copy (|
                                            M.match_operator (|
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::ops::try_trait::Try",
                                                    Ty.apply
                                                      (Ty.path "core::option::Option")
                                                      []
                                                      [ Ty.path "u64" ],
                                                    [],
                                                    "branch",
                                                    []
                                                  |),
                                                  [
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.path "u64",
                                                        "checked_mul",
                                                        []
                                                      |),
                                                      [
                                                        M.read (|
                                                          M.SubPointer.get_struct_record_field (|
                                                            M.read (| self |),
                                                            "core::num::dec2flt::number::Number",
                                                            "mantissa"
                                                          |)
                                                        |);
                                                        M.read (|
                                                          M.SubPointer.get_array_field (|
                                                            M.get_constant (|
                                                              "core::num::dec2flt::number::INT_POW10"
                                                            |),
                                                            M.alloc (|
                                                              M.rust_cast (M.read (| shift |))
                                                            |)
                                                          |)
                                                        |)
                                                      ]
                                                    |)
                                                  ]
                                                |)
                                              |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let γ0_0 :=
                                                      M.SubPointer.get_struct_tuple_field (|
                                                        γ,
                                                        "core::ops::control_flow::ControlFlow::Break",
                                                        0
                                                      |) in
                                                    let residual := M.copy (| γ0_0 |) in
                                                    M.alloc (|
                                                      M.never_to_any (|
                                                        M.read (|
                                                          M.return_ (|
                                                            M.call_closure (|
                                                              M.get_trait_method (|
                                                                "core::ops::try_trait::FromResidual",
                                                                Ty.apply
                                                                  (Ty.path "core::option::Option")
                                                                  []
                                                                  [ F ],
                                                                [
                                                                  Ty.apply
                                                                    (Ty.path "core::option::Option")
                                                                    []
                                                                    [
                                                                      Ty.path
                                                                        "core::convert::Infallible"
                                                                    ]
                                                                ],
                                                                "from_residual",
                                                                []
                                                              |),
                                                              [ M.read (| residual |) ]
                                                            |)
                                                          |)
                                                        |)
                                                      |)
                                                    |)));
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let γ0_0 :=
                                                      M.SubPointer.get_struct_tuple_field (|
                                                        γ,
                                                        "core::ops::control_flow::ControlFlow::Continue",
                                                        0
                                                      |) in
                                                    let val := M.copy (| γ0_0 |) in
                                                    val))
                                              ]
                                            |)
                                          |) in
                                        let~ _ :=
                                          M.match_operator (|
                                            M.alloc (| Value.Tuple [] |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ :=
                                                    M.use
                                                      (M.alloc (|
                                                        BinOp.gt (|
                                                          M.read (| mantissa |),
                                                          M.read (|
                                                            M.get_constant (|
                                                              "core::num::dec2flt::float::RawFloat::MAX_MANTISSA_FAST_PATH"
                                                            |)
                                                          |)
                                                        |)
                                                      |)) 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::option::Option::None"
                                                            []
                                                        |)
                                                      |)
                                                    |)
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                            ]
                                          |) in
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::ops::arith::Mul",
                                              F,
                                              [ F ],
                                              "mul",
                                              []
                                            |),
                                            [
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::num::dec2flt::float::RawFloat",
                                                  F,
                                                  [],
                                                  "from_u64",
                                                  []
                                                |),
                                                [ M.read (| mantissa |) ]
                                              |);
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::num::dec2flt::float::RawFloat",
                                                  F,
                                                  [],
                                                  "pow10_fast_path",
                                                  []
                                                |),
                                                [
                                                  M.rust_cast
                                                    (M.read (|
                                                      M.get_constant (|
                                                        "core::num::dec2flt::float::RawFloat::MAX_EXPONENT_FAST_PATH"
                                                      |)
                                                    |))
                                                ]
                                              |)
                                            ]
                                          |)
                                        |)))
                                  ]
                                |)
                              |) in
                            let~ _ :=
                              M.match_operator (|
                                M.alloc (| Value.Tuple [] |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ :=
                                        M.use
                                          (M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "core::num::dec2flt::number::Number",
                                            "negative"
                                          |)) in
                                      let _ :=
                                        M.is_constant_or_break_match (|
                                          M.read (| γ |),
                                          Value.Bool true
                                        |) in
                                      let~ _ :=
                                        M.write (|
                                          value,
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::ops::arith::Neg",
                                              F,
                                              [],
                                              "neg",
                                              []
                                            |),
                                            [ M.read (| value |) ]
                                          |)
                                        |) in
                                      M.alloc (| Value.Tuple [] |)));
                                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                ]
                              |) in
                            M.alloc (|
                              Value.StructTuple "core::option::Option::Some" [ M.read (| value |) ]
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                      ]
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_try_fast_path :
          M.IsAssociatedFunction Self "try_fast_path" try_fast_path.
      End Impl_core_num_dec2flt_number_Number.
    End number.
  End dec2flt.
End num.
