Check whether a constructor argument is named or anonymous

Stream: general

[Jannis Limperg]

For a tactic I'm writing, I need to know whether each argument of a given constructor is named or not. However, it seems that leaving an argument unnamed and naming it a produce the same result:

inductive I : Type
| intro : unit → I

inductive J : Type
| intro (a : unit) : J

namespace tactic

meta def check : tactic unit := do
(expr.pi n  b  _ _) ← infer_type `(I.intro),
(expr.pi n' b' _ _) ← infer_type `(J.intro),
trace (n = n' ∧ b = b' : bool)

end tactic

run_cmd tactic.check

It seems like the elaborator makes up a name for the unnamed argument of I.intro. Any suggestions for how I could deal with this?

[Simon Hudon]

In kernel terms, named / unnamed is not a meaningful distinction. You can however distinguish between dependent and non-dependent. In (expr.pi n _ d b) ← infer_type (I.intro),, you can check b.has_varto see if the variable named by n is referenced in b`. If it is, you have a dependent product, otherwise, it's a simple function arrow / implication.

[Jannis Limperg]

I feared that would be the answer. Dependent/non-dependent is unfortunately not fine enough for my application. Might have to hack around this. Thanks for the explanation though!