Yiming Xu (Oct 21 2024 at 05:12): Yiming Xu (Oct 21 2024 at 05:12):When I use find_theorems, only the first 40 are displayed. As shown here:
May I please ask if there is any method to display all of them? I have searched online but have not found anything yet.
Mathias Fleury (Oct 21 2024 at 05:16):Control-click on the find_theorems commands shows how it is defined and you can see that there a parameter called opt_lim, which is passed in parenthesis as argument:
find_theorems(68) trancl
That being said, it is way more useful to write a more specific pattern (you can use _, ?a, and so on) to reduce the amount of found theorems
Mathias Fleury (Oct 21 2024 at 05:18):(BTW, I really had to check the code too, because I did not know that this parameter exists: I only write more precise patterns)
Yiming Xu (Oct 21 2024 at 05:23):Thanks for the swift answer! That works well! When I am not such certain for conventions and would like to see more things for a hint, instead have something precise in my mind, I do want to see many theorems that might severs a a hint.
Mathias Fleury (Oct 21 2024 at 05:28):You can also write multiple hints patterns
Yiming Xu (Oct 21 2024 at 05:29):For example?
Mathias Fleury (Oct 21 2024 at 05:29):find_theorems trancl "_ ⊆ _" "_ ∩ _"
that search for all theorems involving trancl, inclusion, and intersection, at any position
Yiming Xu (Oct 21 2024 at 05:30):That is cool!
Mathias Fleury (Oct 21 2024 at 05:30):And the version where you have some idea of the name:
find_theorems "_ ⊆ _" "_ ∩ _" name:trancl
Oh they can even be combined!
Yiming Xu (Oct 21 2024 at 05:33):Wirklich cool. Thanks!
Yong Kiam (Oct 21 2024 at 05:33):Yiming Xu said:
When I use find_theorems, only the first 40 are displayed. As shown here:
May I please ask if there is any method to display all of them? I have searched online but have not found anything yet.
in the Query panel there's a box where you can change the limit for your entire session. What I usually do is add a 0 behind the 40
Mathias Fleury (Oct 21 2024 at 05:34):and stuff can be combined in the Query panel too
Yiming Xu (Oct 21 2024 at 05:35):
Yiming Xu (Oct 21 2024 at 05:35):Still looking for it. Is it on the top bar?
Mathias Fleury (Oct 21 2024 at 05:36):The query panel?
Yiming Xu (Oct 21 2024 at 05:36):
Or
Mathias Fleury (Oct 21 2024 at 05:36):it is a panel so it is a the bottom
Yiming Xu (Oct 21 2024 at 05:37):
Mathias Fleury (Oct 21 2024 at 05:37):or at the right by default, don't remember
Yiming Xu (Oct 21 2024 at 05:37):Aha here it is.
Mathias Fleury (Oct 21 2024 at 05:38):Something rarely useful, but important to notice: even if it looks like it is position independent, the panel only searches for theorems defined at the last position you cursor in the theory file
Yiming Xu (Oct 21 2024 at 05:40):Mathias Fleury said:
Something rarely useful, but important to notice: even if it looks like it is position-independent, the panel only searches at the last position of you cursor in the theory file
I see. I am still to get used to the feature of position-dependent. It can be sometimes confusing. And forces me to get everything compile at any time.
Yiming Xu (Oct 21 2024 at 05:40):A big change for a HOL4 user...
Last updated: Dec 21 2024 at 16:20 UTC