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: Oct 13 2024 at 01:02 UTC