Stream: Coq users

Topic: ✔ Search without a module

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?

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?

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?

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)

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.

Julin S (Jun 13 2022 at 09:09):

Thanks!

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:

Notification Bot (Jun 13 2022 at 09:10):

Julin S has marked this topic as resolved.

Last updated: Oct 13 2024 at 01:02 UTC