When to use withContext

Stream: lean4

[Dan Velleman]

How do you tell when you need to use withContext? In some cases, it seems clear. For example, the description of getLocalDeclFromUserName says that it returns the free variable's declaration "in the current local context," so it seems clear that you need to set the local context before calling it. But what about elabTerm? The description says that it elaborates the syntax "in the current MVarContext," but the syntax might contain references to free variables, so might it need access to the local context? What about unfoldDefinition? If it's being applied to an expression that contains fvars, does it need access to the local context? What about inferType? Surely if an expression contains free variables, you need access to their local declarations to determine the type of the expression? Is there some handy list of functions that have to go inside withContext?

[Mario Carneiro]

Basically everything?

[Mario Carneiro]

Most functions that are in MetaM are that way because they require some local context

[Mario Carneiro]

so you should think about what context you are working on

[Mario Carneiro]

unfoldDefinition requires the context because it calls whnf

[Mario Carneiro]

Anything that handles an Expr is likely to need a local context