Stream: Beginner Questions

Topic: Cannot find a constant "count"

Yiming Xu (Nov 17 2024 at 18:26):

I used "find_consts" to search for a constant that does the same thing as the count in the following.

 (("pred_set", "count_def"), (⊢ ∀n. count n = {m | m < n}, Def))

I used: find_consts "nat ⇒ nat set", but the one it finds is set_decode, not what I want. I would be surprised if this thing does not exist in Isabelle. So does it exist somewhere?

Jonathan Julian Huerta y Munive (Nov 17 2024 at 20:29):

Searching for "{_. _ ≤ _}" led me to atLeast_def. Alternatively, searching for

"_ < _"  "_ ∈ _"

leads to lessThan_iff. Is this what you are looking for?

Yiming Xu (Nov 17 2024 at 20:40):

Thanks a lot! It is very close! I would like the function such that it takes n, and gives the set {x. x < n}. I checked where atLeast lives in, and find that what I want is lessThan.

Yiming Xu (Nov 17 2024 at 20:40):

But why cannot I find such constants using find_consts "nat ⇒ nat set"?

Yiming Xu (Nov 17 2024 at 20:41):

Because it will not attempt to do any type class instantiation? I just checked the type is 'a => 'a set.

Last updated: Nov 01 2025 at 04:23 UTC