Zulip Chat Archive

Stream: general

Topic: Check whether a constructor argument is named or anonymous


view this post on Zulip Jannis Limperg (Apr 14 2020 at 01:37):

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?

view this post on Zulip Simon Hudon (Apr 14 2020 at 04:18):

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.

view this post on Zulip Jannis Limperg (Apr 14 2020 at 13:11):

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!


Last updated: May 11 2021 at 13:22 UTC