Are meta-variables needed in the concrete syntax?

[gabrielhdt]

Currently in Lambdapi, meta-variables may be input with

• ?M[e] which creates a meta-variable of name M in which bound variables e may appear;
• _ which creates a meta-variable where all the bound variables of the current context may appear.

Meta-variables may appear non linearly into terms, the non linearity being specified by the name: f ?M ?M. Are such non-linear meta-variables useful? What's more, using non linear meta-variables can be error prone, since a meta-variable may appear in different contexts.

Are there cases where named meta-variables are required over wildcards, other than with the focus tactic?

[fblanqui]

Named metavariables are useful for giving user names to goals. This is important for proof robustness.
Now, we could perhaps decide to forbid non-linear (wrt metavariables) terms as they could perhaps be dealt with in a different way: refine f ?M ?M; focus M; proof of ?M could be replaced by refine f ?M ?N; focus N; refine ?M; focus M; proof of ?M.

[gabrielhdt]

Do you think this case would happen a lot in practice? Can't we use a let expression to replicate the proof?

[fblanqui]

Why do you want to get rid of named metavariables?

[gabrielhdt]

I'm fine with named metavariables, it's with non linear metavariables that I'm concerned.