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?
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_var
to 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 (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