Stream: Beginner Questions

Topic: extend_nat


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip zibo yang (Jun 02 2021 at 13:16):

Wenda Li said:

In src/HOL/Library, there are Extended_Nat.thy, Extended_Nonnegative_Real.thy, and Extended_Real.thy.

thanks


Last updated: Sep 25 2022 at 22:23 UTC