Zulip Chat Archive

Stream: general

Topic: tactic.to_expr

Edward Ayers (Dec 11 2018 at 17:33):

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 (Dec 11 2018 at 18:22):

Do you need to go through to_expr?

Rob Lewis (Dec 11 2018 at 18:22):

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

Reid Barton (Dec 11 2018 at 18:25):

I was going to suggest

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

Rob Lewis (Dec 11 2018 at 18:42):

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

Last updated: Aug 03 2023 at 10:10 UTC