tactic.to_expr

Stream: general

[Edward Ayers]

How can I get tactic.to_expr to not apply metavariables to implicit arguments? That is;

constant α : Type
axiom P : ∀ {a:α}, a = a
run_cmd do
    p ← tactic.resolve_name `P,
    e ← tactic.to_expr p,
    t ← tactic.infer_type e,
    trace t,  -- gives "?m_1 = ?m_1"
    pure ()

I really want to find a way of getting trace t to say ∀ {a:α}, a = a given only the declaration name P

[Reid Barton]

Do you need to go through to_expr?

[Rob Lewis]

e ← tactic.to_expr p.mk_explicit should work for this case.

[Reid Barton]

I was going to suggest

run_cmd do
    d ← get_decl `P,
    trace d.type,
    pure ()

[Rob Lewis]

Yeah, that's better here, although I guess it depends on the real context.