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

Module num.
  Module overflow_panic.
    (*
    pub const fn add() -> ! {
        panic!("attempt to add with overflow")
    }
    *)
    Definition add (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (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 "attempt to add with overflow" |) ]
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_add : M.IsFunction "core::num::overflow_panic::add" add.
    
    (*
    pub const fn sub() -> ! {
        panic!("attempt to subtract with overflow")
    }
    *)
    Definition sub (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (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 "attempt to subtract with overflow" |) ]
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_sub : M.IsFunction "core::num::overflow_panic::sub" sub.
    
    (*
    pub const fn mul() -> ! {
        panic!("attempt to multiply with overflow")
    }
    *)
    Definition mul (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (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 "attempt to multiply with overflow" |) ]
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_mul : M.IsFunction "core::num::overflow_panic::mul" mul.
    
    (*
    pub const fn div() -> ! {
        panic!("attempt to divide with overflow")
    }
    *)
    Definition div (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (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 "attempt to divide with overflow" |) ]
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_div : M.IsFunction "core::num::overflow_panic::div" div.
    
    (*
    pub const fn rem() -> ! {
        panic!("attempt to calculate the remainder with overflow")
    }
    *)
    Definition rem (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (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 "attempt to calculate the remainder with overflow" |)
                      ]
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_rem : M.IsFunction "core::num::overflow_panic::rem" rem.
    
    (*
    pub const fn neg() -> ! {
        panic!("attempt to negate with overflow")
    }
    *)
    Definition neg (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (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 "attempt to negate with overflow" |) ]
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_neg : M.IsFunction "core::num::overflow_panic::neg" neg.
    
    (*
    pub const fn shr() -> ! {
        panic!("attempt to shift right with overflow")
    }
    *)
    Definition shr (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (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 "attempt to shift right with overflow" |) ]
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_shr : M.IsFunction "core::num::overflow_panic::shr" shr.
    
    (*
    pub const fn shl() -> ! {
        panic!("attempt to shift left with overflow")
    }
    *)
    Definition shl (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (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 "attempt to shift left with overflow" |) ]
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_shl : M.IsFunction "core::num::overflow_panic::shl" shl.
  End overflow_panic.
End num.
