exact name

Stream: metaprogramming / tactics

[Matthew Ballard]

I have n : name in the environment but not in the local context. What is the idiomatic way to achieve exact n?

[Eric Rodriguez]

resolve_name n >>= tactic.exact?

[Rob Lewis]

mk_const instead of resolve_name, probably, exact wants an expr

[Matthew Ballard]

I can call to_expr from resolve_name to get it.

[Rob Lewis]

Yes, that should be equivalent to mk_const n >>= tactic.exact

[Matthew Ballard]

Yeah, mk_const was what I was looking for the past few hours.

[Matthew Ballard]

Thanks @Eric Rodriguez and @Rob Lewis :pray: