CODEWITHSUNDEEP
coq
Ifaz Kabir
Ifaz Kabir

Reputation: 134

Current required number of arguments for unfolding by `simpl`

The Coq Reference Manual details how to use the Arguments directive with a / to mark a constant to be unfolded by the simpl tactic only if enough arguments are supplied.

Is there a way to see how many arguments arguments a constant currently requires to be unfolded?

Similarly, is there a way to see if a constant was flagged to never be simplified by simpl?

Upvotes: 1

Views: 47

Answers (1)

Tej Chajed
Tej Chajed

Reputation: 3948

The About vernacular gives this information (and other useful things):

Definition foo (n:nat) := n.
Arguments foo n/.
About foo.

Arguments foo/.
About foo.

Arguments foo : simpl never.
About foo.

Specifically the output includes "The reduction tactics unfold foo when applied to 1 argument", "...always unfold foo", and "never unfold foo".

Upvotes: 1

Related Questions