## Stream: metaprogramming / tactics

### Topic: matching binders

#### Reid Barton (Oct 18 2020 at 16:53):

Is something like

meta def foo : expr → tactic expr
| (Σ (_ : %%A), %%B) := failed
| _ := failed


ever a good idea? Or will B end up in some weird state (it should be an expression in a modified context)? Should I just use open_lambdas?

#### Simon Hudon (Oct 18 2020 at 16:59):

B will be an open term with one free de Bruijn variable. It's easy to repair. You can also match sigma applied to a lambda and use open_lambdas if you prefer. That seems over kill to me

#### Reid Barton (Oct 18 2020 at 17:01):

Just to check, by "match sigma applied to a lambda" you mean "match sigma applied to a variable, which I expect to be a lambda" right?

#### Reid Barton (Oct 18 2020 at 17:02):

In the MWE, everything is overkill :upside_down:

#### Simon Hudon (Oct 18 2020 at 17:02):

To be even more exact: "match sigma applied to a term, which I expect to be a lambda"

right

#### Reid Barton (Oct 18 2020 at 17:02):

a term (which is the antiquotation of a variable)

#### Simon Hudon (Oct 18 2020 at 17:03):

I would say if you have only one bound variable, I wouldn't use open_*. If you have a few, you might need to write a specialized open_sigma function

#### Reid Barton (Oct 18 2020 at 17:04):

How do I "repair" B if I matched on it?

#### Mario Carneiro (Oct 18 2020 at 17:04):

expr.instantiate_local I think

#### Simon Hudon (Oct 18 2020 at 17:05):

do v <- mk_local_def v A,
let B := B.instantiate_var v,
...


aha

#### Reid Barton (Oct 18 2020 at 17:06):

/-- instantiate_var a b takes the 0th de-Bruijn variable in a and replaces each occurrence with b. -/


#### Simon Hudon (Oct 18 2020 at 17:06):

Be careful, if B contains meta variables, the result will be messed up. You should use instantiate_mvars on B first.

#### Simon Hudon (Oct 18 2020 at 17:08):

Mario Carneiro said:

expr.instantiate_local I think

This is what you use when you're specifying a local constant to instantiate rather than a de Bruijn variable

#### Simon Hudon (Oct 18 2020 at 17:08):

There are a bunch of variations on abstract and instantiate, they're often easy to confuse for each other. (and not to mention kabstract)

#### Reid Barton (Oct 18 2020 at 17:20):

I want to think of B as a type in the context i : A anyways, and recurse on the structure of B, so maybe keeping B in this "open" form while I do the recursion is sensible anyways.
(I guess the alternative is, if i got turned into a local constant, then I need to recognize the variable i in the local_const case of expr.)

#### Simon Hudon (Oct 18 2020 at 17:25):

If you keep B open, tactics like infer_type and unify and anything that uses them breaks down. You may want to carry around a list of new locals instead

#### Reid Barton (Oct 18 2020 at 17:30):

Ah, that might be a problem, since expr doesn't have type information everywhere (e.g., not at app)

#### Simon Hudon (Oct 18 2020 at 17:31):

Exactly

Last updated: May 09 2021 at 23:10 UTC