Search to look for patterns of theorems, is it possible to exclude theorems from a particular module?
Or to look for theorems only from a particular module?
Suppose I had done
Require Import Arith. but at some point doesn't want to use theorems defined there but need to look in other modules. Is there a way?
Search-ing, is it possible to say that the definiton starts/ends with a paritcular term?
Search (_ -> False) shouldn't give things like
A -> (A -> False) -> False but only stuff like
A -> False and
A -> B -> False.
Is it possible?
I think what you are looking for is the
concl:False pattern (see the documentation of search)
Search (_ + _) in Arith (or
Search (_ + _) inside Arith if your Coq version is slightly older) and also
Search (_ + _) outside Arith.
The docs for that sure looks extensive. It will be some time before I get hold of them. :sweat_smile:
Julin S has marked this topic as resolved.
Last updated: Dec 05 2023 at 12:01 UTC