zibo yang (Jun 01 2021 at 22:18): zibo yang (Jun 01 2021 at 22:18):Hi! I am wondering if there exists some extend natural number or integer type in our library like: extend_nat = nat + infinite or extend_int = int + infinite?
Wenda Li (Jun 02 2021 at 02:43):In src/HOL/Library, there are Extended_Nat.thy, Extended_Nonnegative_Real.thy, and Extended_Real.thy.
zibo yang (Jun 02 2021 at 13:16):Wenda Li said:
In
src/HOL/Library, there areExtended_Nat.thy,Extended_Nonnegative_Real.thy, andExtended_Real.thy.
thanks
Last updated: Dec 07 2025 at 08:27 UTC