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

Module i128.
  Definition value_MIN : Value.t := M.run ltac:(M.monadic (M.get_constant (| "core::num::MIN" |))).
  
  Definition value_MAX : Value.t := M.run ltac:(M.monadic (M.get_constant (| "core::num::MAX" |))).
End i128.

Module i16.
  Definition value_MIN : Value.t := M.run ltac:(M.monadic (M.get_constant (| "core::num::MIN" |))).
  
  Definition value_MAX : Value.t := M.run ltac:(M.monadic (M.get_constant (| "core::num::MAX" |))).
End i16.

Module i32.
  Definition value_MIN : Value.t := M.run ltac:(M.monadic (M.get_constant (| "core::num::MIN" |))).
  
  Definition value_MAX : Value.t := M.run ltac:(M.monadic (M.get_constant (| "core::num::MAX" |))).
End i32.

Module i64.
  Definition value_MIN : Value.t := M.run ltac:(M.monadic (M.get_constant (| "core::num::MIN" |))).
  
  Definition value_MAX : Value.t := M.run ltac:(M.monadic (M.get_constant (| "core::num::MAX" |))).
End i64.

Module i8.
  Definition value_MIN : Value.t := M.run ltac:(M.monadic (M.get_constant (| "core::num::MIN" |))).
  
  Definition value_MAX : Value.t := M.run ltac:(M.monadic (M.get_constant (| "core::num::MAX" |))).
End i8.

Module isize.
  Definition value_MIN : Value.t := M.run ltac:(M.monadic (M.get_constant (| "core::num::MIN" |))).
  
  Definition value_MAX : Value.t := M.run ltac:(M.monadic (M.get_constant (| "core::num::MAX" |))).
End isize.

Module u128.
  Definition value_MIN : Value.t := M.run ltac:(M.monadic (M.get_constant (| "core::num::MIN" |))).
  
  Definition value_MAX : Value.t := M.run ltac:(M.monadic (M.get_constant (| "core::num::MAX" |))).
End u128.

Module u16.
  Definition value_MIN : Value.t := M.run ltac:(M.monadic (M.get_constant (| "core::num::MIN" |))).
  
  Definition value_MAX : Value.t := M.run ltac:(M.monadic (M.get_constant (| "core::num::MAX" |))).
End u16.

Module u32.
  Definition value_MIN : Value.t := M.run ltac:(M.monadic (M.get_constant (| "core::num::MIN" |))).
  
  Definition value_MAX : Value.t := M.run ltac:(M.monadic (M.get_constant (| "core::num::MAX" |))).
End u32.

Module u64.
  Definition value_MIN : Value.t := M.run ltac:(M.monadic (M.get_constant (| "core::num::MIN" |))).
  
  Definition value_MAX : Value.t := M.run ltac:(M.monadic (M.get_constant (| "core::num::MAX" |))).
End u64.

Module u8.
  Definition value_MIN : Value.t := M.run ltac:(M.monadic (M.get_constant (| "core::num::MIN" |))).
  
  Definition value_MAX : Value.t := M.run ltac:(M.monadic (M.get_constant (| "core::num::MAX" |))).
End u8.

Module usize.
  Definition value_MIN : Value.t := M.run ltac:(M.monadic (M.get_constant (| "core::num::MIN" |))).
  
  Definition value_MAX : Value.t := M.run ltac:(M.monadic (M.get_constant (| "core::num::MAX" |))).
End usize.
