Stream: Coq users

Topic: ✔ Search without a module


view this post on Zulip Julin S (Jun 13 2022 at 06:56):

While using 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?

view this post on Zulip Julin S (Jun 13 2022 at 06:57):

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?

view this post on Zulip Julin S (Jun 13 2022 at 07:12):

And while Search-ing, is it possible to say that the definiton starts/ends with a paritcular term?

For example, Search (_ -> False) shouldn't give things like A -> (A -> False) -> False but only stuff like A -> False and A -> B -> False.

Is it possible?

view this post on Zulip Kenji Maillard (Jun 13 2022 at 07:59):

I think what you are looking for is the concl:False pattern (see the documentation of search)

view this post on Zulip Ana de Almeida Borges (Jun 13 2022 at 08:50):

You can Search (_ + _) in Arith (or Search (_ + _) inside Arith if your Coq version is slightly older) and also Search (_ + _) outside Arith.

view this post on Zulip Julin S (Jun 13 2022 at 09:09):

Thanks!

view this post on Zulip Julin S (Jun 13 2022 at 09:10):

The docs for that sure looks extensive. It will be some time before I get hold of them. :sweat_smile:

view this post on Zulip Notification Bot (Jun 13 2022 at 09:10):

Julin S has marked this topic as resolved.


Last updated: Jun 20 2024 at 13:02 UTC