mk_meta_var

Stream: general

[Paul-Nicolas Madelaine]

Hi everyone,

I don't really understand how the mk_meta_var tactic works.
Sometimes it adds the meta variable to the list of goals, and sometimes it doesn't, and I don't understand when and why.
Can someone give me more details about its behaviour?

[Mario Carneiro]

mk_meta_var just creates a metavariable, it doesn't add it to the goal list. Goals are controlled directly via get_goals and set_goals

[Paul-Nicolas Madelaine]

@Mario Carneiro indeed you're right, I played with my code a bit more, and it appears that they are not added if I just create them.
But if I use them to build another expression, sometimes they are added to the list of goals automatically, and sometimes not. Do you have an idea of what's happening there?

[Mario Carneiro]

Many of the lean primitive tactics also add the metavars as goals; probably to_expr is responsible. There are flags to adjust what it does with the metavars

[Paul-Nicolas Madelaine]

@Mario Carneiro that's what was happening, thank you!