Stream: Coq users

Topic: Searching for a `Fixpoint`


view this post on Zulip Pierre Rousselin (Apr 27 2024 at 07:39):

In the following:

From Coq Require Import PeanoNat.
Search (nat -> nat -> nat) is:Definition.

I want to list binary operators on nat. It looks like Fixpoints do not appear. But is:Fixpoint is not accepted by Search. Is there another way to list Fixpoints or should I write an issue?

view this post on Zulip Gaëtan Gilbert (Apr 27 2024 at 11:06):

open an issue

view this post on Zulip Gaëtan Gilbert (Apr 27 2024 at 11:06):

or a PR adding Fixpoint to extended_def_token in g_vernac


Last updated: Jun 23 2024 at 04:03 UTC