Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: exact name

Matthew Ballard (Feb 07 2022 at 21:22):

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

Eric Rodriguez (Feb 07 2022 at 21:26):

resolve_name n >>= tactic.exact?

Rob Lewis (Feb 07 2022 at 21:27):

mk_const instead of resolve_name, probably, exact wants an expr

Matthew Ballard (Feb 07 2022 at 21:28):

I can call to_expr from resolve_name to get it.

Rob Lewis (Feb 07 2022 at 21:29):

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

Matthew Ballard (Feb 07 2022 at 21:30):

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

Matthew Ballard (Feb 07 2022 at 21:31):

Thanks @Eric Rodriguez and @Rob Lewis :pray:

Last updated: Dec 20 2023 at 11:08 UTC