coq - Current required number of arguments for unfolding by `simpl`

Question

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?

Answer 1

About白话提供了这些信息（和其他有用的东西）：

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

Arguments foo/.
About foo.

Arguments foo : simpl never.
About foo.

具体来说，输出包括“应用到 1 个参数时展开 foo 的缩减策略”、“...总是展开 foo”和“从不展开 foo”。