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?

In `src/HOL/Library`

, there are `Extended_Nat.thy`

, `Extended_Nonnegative_Real.thy`

, and `Extended_Real.thy`

.

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